TcValidity.hs 80.8 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-}
5

6
{-# LANGUAGE CPP, TupleSections, ViewPatterns #-}
7

8 9
module TcValidity (
  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
10
  ContextKind(..), expectedKindInCtxt,
11
  checkValidTheta, checkValidFamPats,
12
  checkValidInstance, checkValidInstHead, validDerivPred,
13
  checkInstTermination, checkTySynRhs,
14
  ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
15
  checkValidTyFamEqn,
16
  arityErr, badATErr,
17 18
  checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds,
  allDistinctTyVars
19 20 21 22
  ) where

#include "HsVersions.h"

23 24
import GhcPrelude

25 26
import Maybes

27
-- friends:
28
import TcUnify    ( tcSubType_NC )
29
import TcSimplify ( simplifyAmbiguityCheck )
30 31
import TyCoRep
import TcType hiding ( sizeType, sizeTypes )
32
import TcMType
33
import PrelNames
34
import Type
35
import Coercion
36 37 38 39 40 41 42 43
import Kind
import CoAxiom
import Class
import TyCon

-- others:
import HsSyn            -- HsType
import TcRnMonad        -- TcType, amongst others
44
import TcEnv       ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv )
45
import FunDeps
46
import InstEnv     ( InstMatch, lookupInstEnv )
Jan Stolarek's avatar
Jan Stolarek committed
47 48 49
import FamInstEnv  ( isDominatedBy, injectiveBranches,
                     InjectivityCheckResult(..) )
import FamInst     ( makeInjectivityErrors )
50 51 52
import Name
import VarEnv
import VarSet
David Feuer's avatar
David Feuer committed
53
import UniqSet
54
import Var         ( TyVarBndr(..), mkTyVar )
55 56 57 58 59 60
import ErrUtils
import DynFlags
import Util
import ListSetOps
import SrcLoc
import Outputable
61
import Module
62
import Unique      ( mkAlphaTyVarUnique )
63
import qualified GHC.LanguageExtensions as LangExt
64 65 66

import Control.Monad
import Data.List        ( (\\) )
67
import qualified Data.List.NonEmpty as NE
68

Austin Seipp's avatar
Austin Seipp committed
69 70 71
{-
************************************************************************
*                                                                      *
72
          Checking for ambiguity
Austin Seipp's avatar
Austin Seipp committed
73 74
*                                                                      *
************************************************************************
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122

Note [The ambiguity check for type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
checkAmbiguity is a check on *user-supplied type signatures*.  It is
*purely* there to report functions that cannot possibly be called.  So for
example we want to reject:
   f :: C a => Int
The idea is there can be no legal calls to 'f' because every call will
give rise to an ambiguous constraint.  We could soundly omit the
ambiguity check on type signatures entirely, at the expense of
delaying ambiguity errors to call sites.  Indeed, the flag
-XAllowAmbiguousTypes switches off the ambiguity check.

What about things like this:
   class D a b | a -> b where ..
   h :: D Int b => Int
The Int may well fix 'b' at the call site, so that signature should
not be rejected.  Moreover, using *visible* fundeps is too
conservative.  Consider
   class X a b where ...
   class D a b | a -> b where ...
   instance D a b => X [a] b where...
   h :: X a b => a -> a
Here h's type looks ambiguous in 'b', but here's a legal call:
   ...(h [True])...
That gives rise to a (X [Bool] beta) constraint, and using the
instance means we need (D Bool beta) and that fixes 'beta' via D's
fundep!

Behind all these special cases there is a simple guiding principle.
Consider

  f :: <type>
  f = ...blah...

  g :: <type>
  g = f

You would think that the definition of g would surely typecheck!
After all f has exactly the same type, and g=f. But in fact f's type
is instantiated and the instantiated constraints are solved against
the originals, so in the case an ambiguous type it won't work.
Consider our earlier example f :: C a => Int.  Then in g's definition,
we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
and fail.

So in fact we use this as our *definition* of ambiguity.  We use a
very similar test for *inferred* types, to ensure that they are
Gabor Greif's avatar
Gabor Greif committed
123
unambiguous. See Note [Impedance matching] in TcBinds.
124 125 126 127 128 129 130 131 132 133

This test is very conveniently implemented by calling
    tcSubType <type> <type>
This neatly takes account of the functional dependecy stuff above,
and implicit parameter (see Note [Implicit parameters and ambiguity]).
And this is what checkAmbiguity does.

What about this, though?
   g :: C [a] => Int
Is every call to 'g' ambiguous?  After all, we might have
134
   instance C [a] where ...
135 136 137 138 139 140 141 142 143
at the call site.  So maybe that type is ok!  Indeed even f's
quintessentially ambiguous type might, just possibly be callable:
with -XFlexibleInstances we could have
  instance C a where ...
and now a call could be legal after all!  Well, we'll reject this
unless the instance is available *here*.

Note [When to call checkAmbiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
144
We call checkAmbiguity
145 146 147 148
   (a) on user-specified type signatures
   (b) in checkValidType

Conncerning (b), you might wonder about nested foralls.  What about
Simon Peyton Jones's avatar
Simon Peyton Jones committed
149
    f :: forall b. (forall a. Eq a => b) -> b
150
The nested forall is ambiguous.  Originally we called checkAmbiguity
Simon Peyton Jones's avatar
Simon Peyton Jones committed
151 152 153
in the forall case of check_type, but that had two bad consequences:
  * We got two error messages about (Eq b) in a nested forall like this:
       g :: forall a. Eq a => forall b. Eq b => a -> a
Gabor Greif's avatar
Gabor Greif committed
154
  * If we try to check for ambiguity of a nested forall like
Simon Peyton Jones's avatar
Simon Peyton Jones committed
155 156 157 158
    (forall a. Eq a => b), the implication constraint doesn't bind
    all the skolems, which results in "No skolem info" in error
    messages (see Trac #10432).

159
To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
160 161
(I'm still a bit worried about unbound skolems when the type mentions
in-scope type variables.)
162

Simon Peyton Jones's avatar
Simon Peyton Jones committed
163
In fact, because of the co/contra-variance implemented in tcSubType,
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185
this *does* catch function f above. too.

Concerning (a) the ambiguity check is only used for *user* types, not
for types coming from inteface files.  The latter can legitimately
have ambiguous types. Example

   class S a where s :: a -> (Int,Int)
   instance S Char where s _ = (1,1)
   f:: S a => [a] -> Int -> (Int,Int)
   f (_::[a]) x = (a*x,b)
        where (a,b) = s (undefined::a)

Here the worker for f gets the type
        fw :: forall a. S a => Int -> (# Int, Int #)


Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Only a *class* predicate can give rise to ambiguity
An *implicit parameter* cannot.  For example:
        foo :: (?x :: [a]) => Int
        foo = length ?x
Gabor Greif's avatar
Gabor Greif committed
186
is fine.  The call site will supply a particular 'x'
187 188 189 190 191 192 193 194 195 196 197

Furthermore, the type variables fixed by an implicit parameter
propagate to the others.  E.g.
        foo :: (Show a, ?x::[a]) => Int
        foo = show (?x++?x)
The type of foo looks ambiguous.  But it isn't, because at a call site
we might have
        let ?x = 5::Int in foo
and all is well.  In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
Austin Seipp's avatar
Austin Seipp committed
198
-}
199 200 201

checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity ctxt ty
202
  | wantAmbiguityCheck ctxt
203
  = do { traceTc "Ambiguity check for" (ppr ty)
204
         -- Solve the constraints eagerly because an ambiguous type
205
         -- can cause a cascade of further errors.  Since the free
206
         -- tyvars are skolemised, we can safely use tcSimplifyTop
207
       ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
208
       ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
209
                            captureConstraints $
210
                            tcSubType_NC ctxt ty ty
211
       ; simplifyAmbiguityCheck ty wanted
212

213
       ; traceTc "Done ambiguity check for" (ppr ty) }
214 215 216

  | otherwise
  = return ()
217
 where
218
   mk_msg allow_ambiguous
219
     = vcat [ text "In the ambiguity check for" <+> what
220
            , ppUnless allow_ambiguous ambig_msg ]
221
   ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
222 223 224 225 226
   what | Just n <- isSigMaybe ctxt = quotes (ppr n)
        | otherwise                 = pprUserTypeCtxt ctxt

wantAmbiguityCheck :: UserTypeCtxt -> Bool
wantAmbiguityCheck ctxt
227 228 229
  = case ctxt of  -- See Note [When we don't check for ambiguity]
      GhciCtxt     -> False
      TySynCtxt {} -> False
230
      TypeAppCtxt  -> False
231
      _            -> True
232 233

checkUserTypeError :: Type -> TcM ()
234 235 236 237 238 239 240 241
-- Check to see if the type signature mentions "TypeError blah"
-- anywhere in it, and fail if so.
--
-- Very unsatisfactorily (Trac #11144) we need to tidy the type
-- because it may have come from an /inferred/ signature, not a
-- user-supplied one.  This is really only a half-baked fix;
-- the other errors in checkValidType don't do tidying, and so
-- may give bad error messages when given an inferred type.
242 243 244
checkUserTypeError = check
  where
  check ty
245
    | Just msg     <- userTypeError_maybe ty  = fail_with msg
246 247
    | Just (_,ts)  <- splitTyConApp_maybe ty  = mapM_ check ts
    | Just (t1,t2) <- splitAppTy_maybe ty     = check t1 >> check t2
248
    | Just (_,t1)  <- splitForAllTy_maybe ty  = check t1
249 250
    | otherwise                               = return ()

251 252 253 254 255
  fail_with msg = do { env0 <- tcInitTidyEnv
                     ; let (env1, tidy_msg) = tidyOpenType env0 msg
                     ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }


256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
{- Note [When we don't check for ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a few places we do not want to check a user-specified type for ambiguity

* GhciCtxt: Allow ambiguous types in GHCi's :kind command
  E.g.   type family T a :: *  -- T :: forall k. k -> *
  Then :k T should work in GHCi, not complain that
  (T k) is ambiguous!

* TySynCtxt: type T a b = C a b => blah
  It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
  cure the ambiguity.  So we defer the ambiguity check to the use site.

  There is also an implementation reason (Trac #11608).  In the RHS of
  a type synonym we don't (currently) instantiate 'a' and 'b' with
  TcTyVars before calling checkValidType, so we get asertion failures
  from doing an ambiguity check on a type with TyVars in it.  Fixing this
  would not be hard, but let's wait till there's a reason.

275 276 277 278
* TypeAppCtxt: visible type application
     f @ty
  No need to check ty for ambiguity

279

Austin Seipp's avatar
Austin Seipp committed
280 281
************************************************************************
*                                                                      *
282
          Checking validity of a user-defined type
Austin Seipp's avatar
Austin Seipp committed
283 284
*                                                                      *
************************************************************************
285 286

When dealing with a user-written type, we first translate it from an HsType
Austin Seipp's avatar
Austin Seipp committed
287
to a Type, performing kind checking, and then check various things that should
288 289 290
be true about it.  We don't want to perform these checks at the same time
as the initial translation because (a) they are unnecessary for interface-file
types and (b) when checking a mutually recursive group of type and class decls,
Gabor Greif's avatar
Gabor Greif committed
291
we can't "look" at the tycons/classes yet.  Also, the checks are rather
292 293
diverse, and used to really mess up the other code.

Austin Seipp's avatar
Austin Seipp committed
294
One thing we check for is 'rank'.
295 296 297 298 299 300 301 302 303 304 305

        Rank 0:         monotypes (no foralls)
        Rank 1:         foralls at the front only, Rank 0 inside
        Rank 2:         foralls at the front, Rank 1 on left of fn arrow,

        basic ::= tyvar | T basic ... basic

        r2  ::= forall tvs. cxt => r2a
        r2a ::= r1 -> r2a | basic
        r1  ::= forall tvs. cxt => r0
        r0  ::= r0 -> r0 | basic
Austin Seipp's avatar
Austin Seipp committed
306 307

Another thing is to check that type synonyms are saturated.
308 309 310 311
This might not necessarily show up in kind checking.
        type A i = i
        data T k = MkT (k Int)
        f :: T A        -- BAD!
Austin Seipp's avatar
Austin Seipp committed
312
-}
313 314

checkValidType :: UserTypeCtxt -> Type -> TcM ()
315
-- Checks that a user-written type is valid for the given context
Gabor Greif's avatar
Gabor Greif committed
316
-- Assumes argument is fully zonked
317
-- Not used for instance decls; checkValidInstance instead
Austin Seipp's avatar
Austin Seipp committed
318
checkValidType ctxt ty
319
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
320
       ; rankn_flag  <- xoptM LangExt.RankNTypes
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
321
       ; impred_flag <- xoptM LangExt.ImpredicativeTypes
322 323 324 325 326 327 328 329 330 331 332 333 334 335
       ; let gen_rank :: Rank -> Rank
             gen_rank r | rankn_flag = ArbitraryRank
                        | otherwise  = r

             rank1 = gen_rank r1
             rank0 = gen_rank r0

             r0 = rankZeroMonoType
             r1 = LimitedRank True r0

             rank
               = case ctxt of
                 DefaultDeclCtxt-> MustBeMonoType
                 ResSigCtxt     -> MustBeMonoType
336
                 PatSigCtxt     -> rank0
337 338 339
                 RuleSigCtxt _  -> rank1
                 TySynCtxt _    -> rank0

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
340
                 ExprSigCtxt    -> rank1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
341 342 343 344 345 346
                 TypeAppCtxt | impred_flag -> ArbitraryRank
                             | otherwise   -> tyConArgMonoType
                    -- Normally, ImpredicativeTypes is handled in check_arg_type,
                    -- but visible type applications don't go through there.
                    -- So we do this check here.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
347 348 349 350
                 FunSigCtxt {}  -> rank1
                 InfSigCtxt _   -> ArbitraryRank        -- Inferred type
                 ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                         -- constructor, hence rank 1
351
                 PatSynCtxt _   -> rank1
352 353 354 355 356 357 358 359

                 ForSigCtxt _   -> rank1
                 SpecInstCtxt   -> rank1
                 ThBrackCtxt    -> rank1
                 GhciCtxt       -> ArbitraryRank
                 _              -> panic "checkValidType"
                                          -- Can't happen; not used for *user* sigs

niteria's avatar
niteria committed
360
       ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
361

362
        -- Check the internal validity of the type itself
363
       ; check_type env ctxt rank ty
364

365 366
       ; checkUserTypeError ty

367
       -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
368 369
       -- NB: this will happen even for monotypes, but that should be cheap;
       --     and there may be nested foralls for the subtype test to examine
370 371
       ; checkAmbiguity ctxt ty

372
       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
373 374

checkValidMonoType :: Type -> TcM ()
Gabor Greif's avatar
Gabor Greif committed
375
-- Assumes argument is fully zonked
376
checkValidMonoType ty
niteria's avatar
niteria committed
377
  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
378
       ; check_type env SigmaCtxt MustBeMonoType ty }
379

380 381 382
checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
checkTySynRhs ctxt ty
  | returnsConstraintKind actual_kind
383
  = do { ck <- xoptM LangExt.ConstraintKinds
384 385 386
       ; if ck
         then  when (isConstraintKind actual_kind)
                    (do { dflags <- getDynFlags
387 388
                        ; check_pred_ty emptyTidyEnv dflags ctxt ty })
         else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
389 390

  | otherwise
391
  = return ()
392 393 394
  where
    actual_kind = typeKind ty

395 396 397 398 399
-- | The kind expected in a certain context.
data ContextKind = TheKind Kind   -- ^ a specific kind
                 | AnythingKind   -- ^ any kind will do
                 | OpenKind       -- ^ something of the form @TYPE _@

400 401
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
402 403 404 405
expectedKindInCtxt :: UserTypeCtxt -> ContextKind
expectedKindInCtxt (TySynCtxt _)   = AnythingKind
expectedKindInCtxt ThBrackCtxt     = AnythingKind
expectedKindInCtxt GhciCtxt        = AnythingKind
406 407
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in TcEnv
408
expectedKindInCtxt DefaultDeclCtxt = AnythingKind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
409
expectedKindInCtxt TypeAppCtxt     = AnythingKind
410 411 412 413
expectedKindInCtxt (ForSigCtxt _)  = TheKind liftedTypeKind
expectedKindInCtxt InstDeclCtxt    = TheKind constraintKind
expectedKindInCtxt SpecInstCtxt    = TheKind constraintKind
expectedKindInCtxt _               = OpenKind
414

Austin Seipp's avatar
Austin Seipp committed
415
{-
416 417
Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
418
Technically
419 420 421 422
            Int -> forall a. a->a
is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
validity checker allow a forall after an arrow only if we allow it
before -- that is, with Rank2Types or RankNTypes
Austin Seipp's avatar
Austin Seipp committed
423
-}
424 425 426 427 428 429 430 431

data Rank = ArbitraryRank         -- Any rank ok

          | LimitedRank   -- Note [Higher rank types]
                 Bool     -- Forall ok at top
                 Rank     -- Use for function arguments

          | MonoType SDoc   -- Monotype, with a suggestion of how it could be a polytype
Austin Seipp's avatar
Austin Seipp committed
432

433 434
          | MustBeMonoType  -- Monotype regardless of flags

435 436 437 438 439 440

rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
rankZeroMonoType   = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
tyConArgMonoType   = MonoType (text "GHC doesn't yet support impredicative polymorphism")
synArgMonoType     = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
constraintMonoType = MonoType (text "A constraint must be a monotype")
441 442 443 444 445 446 447 448 449 450 451

funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
funArgResRank other_rank               = (other_rank, other_rank)

forAllAllowed :: Rank -> Bool
forAllAllowed ArbitraryRank             = True
forAllAllowed (LimitedRank forall_ok _) = forall_ok
forAllAllowed _                         = False

----------------------------------------
452
check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
453 454
-- The args say what the *type context* requires, independent
-- of *flag* settings.  You test the flag settings at usage sites.
Austin Seipp's avatar
Austin Seipp committed
455
--
456 457 458
-- Rank is allowed rank for function args
-- Rank 0 means no for-alls anywhere

459
check_type env ctxt rank ty
460
  | not (null tvs && null theta)
461 462
  = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
        ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
Austin Seipp's avatar
Austin Seipp committed
463
                -- Reject e.g. (Maybe (?x::Int => Int)),
464
                -- with a decent error message
465

466
        ; check_valid_theta env' SigmaCtxt theta
467 468 469
                -- Allow     type T = ?x::Int => Int -> Int
                -- but not   type T = ?x::Int

470
        ; check_type env' ctxt rank tau      -- Allow foralls to right of arrow
471
        ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
472 473
                   (forAllEscapeErr env' ty tau_kind)
        }
474 475
  where
    (tvs, theta, tau) = tcSplitSigmaTy ty
476
    tau_kind          = typeKind tau
477
    (env', _)         = tidyTyCoVarBndrs env tvs
478 479 480 481 482

    phi_kind | null theta = tau_kind
             | otherwise  = liftedTypeKind
        -- If there are any constraints, the kind is *. (#11405)

483
check_type _ _ _ (TyVarTy _) = return ()
484

Simon Peyton Jones's avatar
Simon Peyton Jones committed
485
check_type env ctxt rank (FunTy arg_ty res_ty)
486 487
  = do  { check_type env ctxt arg_rank arg_ty
        ; check_type env ctxt res_rank res_ty }
488 489 490
  where
    (arg_rank, res_rank) = funArgResRank rank

491 492 493
check_type env ctxt rank (AppTy ty1 ty2)
  = do  { check_arg_type env ctxt rank ty1
        ; check_arg_type env ctxt rank ty2 }
494

495
check_type env ctxt rank ty@(TyConApp tc tys)
496
  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
497 498 499 500 501
  = check_syn_tc_app env ctxt rank ty tc tys
  | isUnboxedTupleTyCon tc = check_ubx_tuple  env ctxt      ty    tys
  | otherwise              = mapM_ (check_arg_type env ctxt rank) tys

check_type _ _ _ (LitTy {}) = return ()
502

503
check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
504

505
check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
506 507

----------------------------------------
508
check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
509
                 -> TyCon -> [KindOrType] -> TcM ()
510
-- Used for type synonyms and type synonym families,
Austin Seipp's avatar
Austin Seipp committed
511
-- which must be saturated,
512
-- but not data families, which need not be saturated
513
check_syn_tc_app env ctxt rank ty tc tys
514
  | tys `lengthAtLeast` tc_arity   -- Saturated
515 516 517 518 519 520 521
       -- Check that the synonym has enough args
       -- This applies equally to open and closed synonyms
       -- It's OK to have an *over-applied* type synonym
       --      data Tree a b = ...
       --      type Foo a = Tree [a]
       --      f :: Foo a b -> ...
  = do  { -- See Note [Liberal type synonyms]
522
        ; liberal <- xoptM LangExt.LiberalTypeSynonyms
523
        ; if not liberal || isTypeFamilyTyCon tc then
524
                -- For H98 and synonym families, do check the type args
525
                mapM_ check_arg tys
526 527

          else  -- In the liberal case (only for closed syns), expand then check
Ben Gamari's avatar
Ben Gamari committed
528
          case tcView ty of
529
             Just ty' -> check_type env ctxt rank ty'
530 531
             Nothing  -> pprPanic "check_tau_type" (ppr ty)  }

Austin Seipp's avatar
Austin Seipp committed
532
  | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in
533
                      -- GHCi :kind commands; see Trac #7586
534
  = mapM_ check_arg tys
535 536

  | otherwise
537
  = failWithTc (tyConArityErr tc tys)
538 539
  where
    tc_arity  = tyConArity tc
540 541
    check_arg | isTypeFamilyTyCon tc = check_arg_type  env ctxt rank
              | otherwise            = check_type      env ctxt synArgMonoType
Austin Seipp's avatar
Austin Seipp committed
542

543
----------------------------------------
544
check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
545
                -> [KindOrType] -> TcM ()
546
check_ubx_tuple env ctxt ty tys
547
  = do  { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
548
        ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
549

550
        ; impred <- xoptM LangExt.ImpredicativeTypes
551 552 553 554
        ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
                -- c.f. check_arg_type
                -- However, args are allowed to be unlifted, or
                -- more unboxed tuples, so can't use check_arg_ty
555
        ; mapM_ (check_type env ctxt rank') tys }
Austin Seipp's avatar
Austin Seipp committed
556

557
----------------------------------------
558
check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
559 560 561 562 563
-- The sort of type that can instantiate a type variable,
-- or be the argument of a type constructor.
-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
-- Other unboxed types are very occasionally allowed as type
-- arguments depending on the kind of the type constructor
Austin Seipp's avatar
Austin Seipp committed
564
--
565 566 567 568 569 570 571 572 573 574 575 576
-- For example, we want to reject things like:
--
--      instance Ord a => Ord (forall s. T s a)
-- and
--      g :: T s (forall b.b)
--
-- NB: unboxed tuples can have polymorphic or unboxed args.
--     This happens in the workers for functions returning
--     product types with polymorphic components.
--     But not in user code.
-- Anyway, they are dealt with by a special case in check_tau_type

577 578 579
check_arg_type _ _ _ (CoercionTy {}) = return ()

check_arg_type env ctxt rank ty
580
  = do  { impred <- xoptM LangExt.ImpredicativeTypes
581 582 583 584
        ; let rank' = case rank of          -- Predictive => must be monotype
                        MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
                        _other | impred    -> ArbitraryRank
                               | otherwise -> tyConArgMonoType
Austin Seipp's avatar
Austin Seipp committed
585
                        -- Make sure that MustBeMonoType is propagated,
586 587 588 589
                        -- so that we don't suggest -XImpredicativeTypes in
                        --    (Ord (forall a.a)) => a -> a
                        -- and so that if it Must be a monotype, we check that it is!

590
        ; check_type env ctxt rank' ty }
591 592

----------------------------------------
593 594 595
forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
forAllTyErr env rank ty
   = ( env
596
     , vcat [ hang herald 2 (ppr_tidy env ty)
597
            , suggestion ] )
598
  where
599 600 601
    (tvs, _theta, _tau) = tcSplitSigmaTy ty
    herald | null tvs  = text "Illegal qualified type:"
           | otherwise = text "Illegal polymorphic type:"
602
    suggestion = case rank of
603
                   LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
604
                   MonoType d     -> d
605
                   _              -> Outputable.empty -- Polytype is always illegal
606

607 608 609 610 611 612 613 614
forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
forAllEscapeErr env ty tau_kind
  = ( env
    , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
                 , text "(skolem escape)" ])
         2 (vcat [ text "   type:" <+> ppr_tidy env ty
                 , text "of kind:" <+> ppr_tidy env tau_kind ]) )

615 616
ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
ubxArgTyErr env ty = (env, sep [text "Illegal unboxed tuple type as function argument:", ppr_tidy env ty])
617

Austin Seipp's avatar
Austin Seipp committed
618
{-
619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647
Note [Liberal type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
doing validity checking.  This allows us to instantiate a synonym defn
with a for-all type, or with a partially-applied type synonym.
        e.g.   type T a b = a
               type S m   = m ()
               f :: S (T Int)
Here, T is partially applied, so it's illegal in H98.  But if you
expand S first, then T we get just
               f :: Int
which is fine.

IMPORTANT: suppose T is a type synonym.  Then we must do validity
checking on an appliation (T ty1 ty2)

        *either* before expansion (i.e. check ty1, ty2)
        *or* after expansion (i.e. expand T ty1 ty2, and then check)
        BUT NOT BOTH

If we do both, we get exponential behaviour!!

  data TIACons1 i r c = c i ::: r c
  type TIACons2 t x = TIACons1 t (TIACons1 t x)
  type TIACons3 t x = TIACons2 t (TIACons1 t x)
  type TIACons4 t x = TIACons2 t (TIACons2 t x)
  type TIACons7 t x = TIACons4 t (TIACons3 t x)


Austin Seipp's avatar
Austin Seipp committed
648 649
************************************************************************
*                                                                      *
650
\subsection{Checking a theta or source type}
Austin Seipp's avatar
Austin Seipp committed
651 652
*                                                                      *
************************************************************************
653

654 655 656 657 658 659 660 661
Note [Implicit parameters in instance decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Implicit parameters _only_ allowed in type signatures; not in instance
decls, superclasses etc. The reason for not allowing implicit params in
instances is a bit subtle.  If we allowed
  instance (?x::Int, Eq a) => Foo [a] where ...
then when we saw
     (e :: (?x::Int) => t)
Gabor Greif's avatar
Gabor Greif committed
662 663
it would be unclear how to discharge all the potential uses of the ?x
in e.  For example, a constraint Foo [Int] might come out of e, and
664
applying the instance decl would show up two uses of ?x.  Trac #8912.
Austin Seipp's avatar
Austin Seipp committed
665
-}
666

667
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
Edward Z. Yang's avatar
Edward Z. Yang committed
668
-- Assumes argument is fully zonked
669
checkValidTheta ctxt theta
niteria's avatar
niteria committed
670
  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
671 672
       ; addErrCtxtM (checkThetaCtxt ctxt theta) $
         check_valid_theta env ctxt theta }
673 674

-------------------------
675 676
check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
check_valid_theta _ _ []
677
  = return ()
678
check_valid_theta env ctxt theta
679
  = do { dflags <- getDynFlags
680 681 682
       ; warnTcM (Reason Opt_WarnDuplicateConstraints)
                 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
                 (dupPredWarn env dups)
683
       ; traceTc "check_valid_theta" (ppr theta)
684
       ; mapM_ (check_pred_ty env dflags ctxt) theta }
685
  where
niteria's avatar
niteria committed
686 687 688
    (_,dups) = removeDups nonDetCmpType theta
    -- It's OK to use nonDetCmpType because dups only appears in the
    -- warning
689 690

-------------------------
691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714
{- Note [Validity checking for constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We look through constraint synonyms so that we can see the underlying
constraint(s).  For example
   type Foo = ?x::Int
   instance Foo => C T
We should reject the instance because it has an implicit parameter in
the context.

But we record, in 'under_syn', whether we have looked under a synonym
to avoid requiring language extensions at the use site.  Main example
(Trac #9838):

   {-# LANGUAGE ConstraintKinds #-}
   module A where
      type EqShow a = (Eq a, Show a)

   module B where
      import A
      foo :: EqShow a => a -> String

We don't want to require ConstraintKinds in module B.
-}

715
check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
716
-- Check the validity of a predicate in a signature
717
-- See Note [Validity checking for constraints]
718
check_pred_ty env dflags ctxt pred
719
  = do { check_type env SigmaCtxt constraintMonoType pred
720
       ; check_pred_help False env dflags ctxt pred }
721 722

check_pred_help :: Bool    -- True <=> under a type synonym
723
                -> TidyEnv
724 725
                -> DynFlags -> UserTypeCtxt
                -> PredType -> TcM ()
726
check_pred_help under_syn env dflags ctxt pred
Ben Gamari's avatar
Ben Gamari committed
727
  | Just pred' <- tcView pred  -- Switch on under_syn when going under a
728
                                 -- synonym (Trac #9838, yuk)
729
  = check_pred_help True env dflags ctxt pred'
Simon Peyton Jones's avatar
Simon Peyton Jones committed
730 731 732

  | otherwise  -- A bit like classifyPredType, but not the same
               -- E.g. we treat (~) like (~#); and we look inside tuples
733
  = case splitTyConApp_maybe pred of
734 735
      Just (tc, tys)
        | isTupleTyCon tc
736
        -> check_tuple_pred under_syn env dflags ctxt pred tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
737

738 739 740
        | tc `hasKey` heqTyConKey ||
          tc `hasKey` eqTyConKey ||
          tc `hasKey` eqPrimTyConKey
Simon Peyton Jones's avatar
Simon Peyton Jones committed
741 742
          -- NB: this equality check must come first,
          --  because (~) is a class,too.
743
        -> check_eq_pred env dflags pred tc tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
744

745
        | Just cls <- tyConClass_maybe tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
746 747 748
          -- Includes Coercible
        -> check_class_pred env dflags ctxt pred cls tys

749
      _ -> check_irred_pred under_syn env dflags ctxt pred
750

751 752
check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
check_eq_pred env dflags pred tc tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
753 754
  =         -- Equational constraints are valid in all contexts if type
            -- families are permitted
755
    do { checkTc (tys `lengthIs` tyConArity tc) (tyConArityErr tc tys)
756 757
       ; checkTcM (xopt LangExt.TypeFamilies dflags
                   || xopt LangExt.GADTs dflags)
758
                  (eqPredTyErr env pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
759

760 761
check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
check_tuple_pred under_syn env dflags ctxt pred ts
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
762
  = do { -- See Note [ConstraintKinds in predicates]
763
         checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
764 765
                  (predTupleErr env pred)
       ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
766 767
    -- This case will not normally be executed because without
    -- -XConstraintKinds tuple types are only kind-checked as *
768

769 770
check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
check_irred_pred under_syn env dflags ctxt pred
771
    -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
772 773 774 775 776
    -- where X is a type function
  = do { -- If it looks like (x t1 t2), require ConstraintKinds
         --   see Note [ConstraintKinds in predicates]
         -- But (X t1 t2) is always ok because we just require ConstraintKinds
         -- at the definition site (Trac #9838)
777
        failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
778
                                && hasTyVarHead pred)
779
                  (predIrredErr env pred)
780 781 782

         -- Make sure it is OK to have an irred pred in this context
         -- See Note [Irreducible predicates in superclasses]
783
       ; failIfTcM (is_superclass ctxt
784
                    && not (xopt LangExt.UndecidableInstances dflags)
785 786
                    && has_tyfun_head pred)
                   (predSuperClassErr env pred) }
787
  where
788 789 790 791 792
    is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
    has_tyfun_head ty
      = case tcSplitTyConApp_maybe ty of
          Just (tc, _) -> isTypeFamilyTyCon tc
          Nothing      -> False
793 794 795 796 797 798 799 800 801 802 803 804 805

{- Note [ConstraintKinds in predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Don't check for -XConstraintKinds under a type synonym, because that
was done at the type synonym definition site; see Trac #9838
e.g.   module A where
          type C a = (Eq a, Ix a)   -- Needs -XConstraintKinds
       module B where
          import A
          f :: C a => a -> a        -- Does *not* need -XConstraintKinds

Note [Irreducible predicates in superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
806
Allowing type-family calls in class superclasses is somewhat dangerous
807 808 809 810 811 812 813 814
because we can write:

 type family Fooish x :: * -> Constraint
 type instance Fooish () = Foo
 class Fooish () a => Foo a where

This will cause the constraint simplifier to loop because every time we canonicalise a
(Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
815
solved to add+canonicalise another (Foo a) constraint.  -}
816 817

-------------------------
818 819
check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
check_class_pred env dflags ctxt pred cls tys
820
  | isIPClass cls
821
  = do { check_arity
822
       ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
823

824
  | otherwise
825
  = do { check_arity
826 827
       ; warn_simp <- woptM Opt_WarnSimplifiableClassConstraints
       ; when warn_simp check_simplifiable_class_constraint
828
       ; checkTcM arg_tys_ok (predTyVarErr env pred) }
829
  where
830
    check_arity = checkTc (tys `lengthIs` classArity cls)
831
                          (tyConArityErr (classTyCon cls) tys)
832 833

    -- Check the arguments of a class constraint
834 835
    flexible_contexts = xopt LangExt.FlexibleContexts     dflags
    undecidable_ok    = xopt LangExt.UndecidableInstances dflags
836 837
    arg_tys_ok = case ctxt of
        SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
838
        InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
839 840
                                -- Further checks on head and theta
                                -- in checkInstTermination
841
        _            -> checkValidClsArgs flexible_contexts cls tys
842

843 844
    -- See Note [Simplifiable given constraints]
    check_simplifiable_class_constraint
845 846
       | xopt LangExt.MonoLocalBinds dflags
       = return ()
847 848 849
       | DataTyCtxt {} <- ctxt   -- Don't do this check for the "stupid theta"
       = return ()               -- of a data type declaration
       | otherwise
850 851 852 853 854 855 856 857
       = do { envs <- tcGetInstEnvs
            ; case lookupInstEnv False envs cls tys of
                 ([m], [], _) -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
                                           (simplifiable_constraint_warn m)
                 _ -> return () }

    simplifiable_constraint_warn :: InstMatch -> SDoc
    simplifiable_constraint_warn (match, _)
858 859 860
     = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
                 2 (text "matches an instance declaration")
            , ppr match
861 862
            , hang (text "This makes type inference for inner bindings fragile;")
                 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
863 864

{- Note [Simplifiable given constraints]
865
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
866 867 868
A type signature like
   f :: Eq [(a,b)] => a -> b
is very fragile, for reasons described at length in TcInteract
869 870 871 872 873 874 875
Note [Instance and Given overlap].  As that Note discusses, for the
most part the clever stuff in TcInteract means that we don't use a
top-level instance if a local Given might fire, so there is no
fragility. But if we /infer/ the type of a local let-binding, things
can go wrong (Trac #11948 is an example, discussed in the Note).

So this warning is switched on only if we have NoMonoLocalBinds; in
876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896
that case the warning discourages users from writing simplifiable
class constraints.

The warning only fires if the constraint in the signature
matches the top-level instances in only one way, and with no
unifiers -- that is, under the same circumstances that
TcInteract.matchInstEnv fires an interaction with the top
level instances.  For example (Trac #13526), consider

  instance {-# OVERLAPPABLE #-} Eq (T a) where ...
  instance                   Eq (T Char) where ..
  f :: Eq (T a) => ...

We don't want to complain about this, even though the context
(Eq (T a)) matches an instance, because the user may be
deliberately deferring the choice so that the Eq (T Char)
has a chance to fire when 'f' is called.  And the fragility
only matters when there's a risk that the instance might
fire instead of the local 'given'; and there is no such
risk in this case.  Just use the same rules as for instance
firing!
897 898
-}

899 900 901
-------------------------
okIPCtxt :: UserTypeCtxt -> Bool
  -- See Note [Implicit parameters in instance decls]
902 903 904 905 906 907 908 909 910 911 912 913 914
okIPCtxt (FunSigCtxt {})        = True
okIPCtxt (InfSigCtxt {})        = True
okIPCtxt ExprSigCtxt            = True
okIPCtxt TypeAppCtxt            = True
okIPCtxt PatSigCtxt             = True
okIPCtxt ResSigCtxt             = True
okIPCtxt GenSigCtxt             = True
okIPCtxt (ConArgCtxt {})        = True
okIPCtxt (ForSigCtxt {})        = True  -- ??
okIPCtxt ThBrackCtxt            = True
okIPCtxt GhciCtxt               = True
okIPCtxt SigmaCtxt              = True
okIPCtxt (DataTyCtxt {})        = True
915
okIPCtxt (PatSynCtxt {})        = True
916 917
okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
                                         -- Trac #11466
918