TcValidity.hs 80 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, 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 Maybes

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

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

import Control.Monad
import Data.List        ( (\\) )

Austin Seipp's avatar
Austin Seipp committed
66 67 68
{-
************************************************************************
*                                                                      *
69
          Checking for ambiguity
Austin Seipp's avatar
Austin Seipp committed
70 71
*                                                                      *
************************************************************************
72 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

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
120
unambiguous. See Note [Impedance matching] in TcBinds.
121 122 123 124 125 126 127 128 129 130

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
131
   instance C [a] where ...
132 133 134 135 136 137 138 139 140
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
141
We call checkAmbiguity
142 143 144 145
   (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
146
    f :: forall b. (forall a. Eq a => b) -> b
147
The nested forall is ambiguous.  Originally we called checkAmbiguity
Simon Peyton Jones's avatar
Simon Peyton Jones committed
148 149 150 151 152 153 154 155
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
  * If we try to check for ambiguity of an nested forall like
    (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).

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
160
In fact, because of the co/contra-variance implemented in tcSubType,
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
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
183
is fine.  The call site will supply a particular 'x'
184 185 186 187 188 189 190 191 192 193 194

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
195
-}
196 197 198

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

210
       ; traceTc "Done ambiguity check for" (ppr ty) }
211 212 213

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

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

checkUserTypeError :: Type -> TcM ()
230 231 232 233 234 235 236 237
-- 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.
238 239 240
checkUserTypeError = check
  where
  check ty
241
    | Just msg     <- userTypeError_maybe ty  = fail_with msg
242 243
    | Just (_,ts)  <- splitTyConApp_maybe ty  = mapM_ check ts
    | Just (t1,t2) <- splitAppTy_maybe ty     = check t1 >> check t2
244
    | Just (_,t1)  <- splitForAllTy_maybe ty  = check t1
245 246
    | otherwise                               = return ()

247 248 249 250 251
  fail_with msg = do { env0 <- tcInitTidyEnv
                     ; let (env1, tidy_msg) = tidyOpenType env0 msg
                     ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }


252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
{- 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.


Austin Seipp's avatar
Austin Seipp committed
272 273
************************************************************************
*                                                                      *
274
          Checking validity of a user-defined type
Austin Seipp's avatar
Austin Seipp committed
275 276
*                                                                      *
************************************************************************
277 278

When dealing with a user-written type, we first translate it from an HsType
Austin Seipp's avatar
Austin Seipp committed
279
to a Type, performing kind checking, and then check various things that should
280 281 282
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
283
we can't "look" at the tycons/classes yet.  Also, the checks are rather
284 285
diverse, and used to really mess up the other code.

Austin Seipp's avatar
Austin Seipp committed
286
One thing we check for is 'rank'.
287 288 289 290 291 292 293 294 295 296 297

        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
298 299

Another thing is to check that type synonyms are saturated.
300 301 302 303
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
304
-}
305 306

checkValidType :: UserTypeCtxt -> Type -> TcM ()
307
-- Checks that a user-written type is valid for the given context
Gabor Greif's avatar
Gabor Greif committed
308
-- Assumes argument is fully zonked
309
-- Not used for instance decls; checkValidInstance instead
Austin Seipp's avatar
Austin Seipp committed
310
checkValidType ctxt ty
311
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
312
       ; rankn_flag  <- xoptM LangExt.RankNTypes
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
313
       ; impred_flag <- xoptM LangExt.ImpredicativeTypes
314 315 316 317 318 319 320 321 322 323 324 325 326 327
       ; 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
328
                 PatSigCtxt     -> rank0
329 330 331
                 RuleSigCtxt _  -> rank1
                 TySynCtxt _    -> rank0

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
332
                 ExprSigCtxt    -> rank1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
333 334 335 336 337 338
                 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
339 340 341 342
                 FunSigCtxt {}  -> rank1
                 InfSigCtxt _   -> ArbitraryRank        -- Inferred type
                 ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                         -- constructor, hence rank 1
343
                 PatSynCtxt _   -> rank1
344 345 346 347 348 349 350 351

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

niteria's avatar
niteria committed
352
       ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
353

354
        -- Check the internal validity of the type itself
355
       ; check_type env ctxt rank ty
356

357 358
       ; checkUserTypeError ty

359
       -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
360 361
       -- NB: this will happen even for monotypes, but that should be cheap;
       --     and there may be nested foralls for the subtype test to examine
362 363
       ; checkAmbiguity ctxt ty

364
       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
365 366

checkValidMonoType :: Type -> TcM ()
Gabor Greif's avatar
Gabor Greif committed
367
-- Assumes argument is fully zonked
368
checkValidMonoType ty
niteria's avatar
niteria committed
369
  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
370
       ; check_type env SigmaCtxt MustBeMonoType ty }
371

372 373 374
checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
checkTySynRhs ctxt ty
  | returnsConstraintKind actual_kind
375
  = do { ck <- xoptM LangExt.ConstraintKinds
376 377 378
       ; if ck
         then  when (isConstraintKind actual_kind)
                    (do { dflags <- getDynFlags
379 380
                        ; check_pred_ty emptyTidyEnv dflags ctxt ty })
         else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
381 382

  | otherwise
383
  = return ()
384 385 386
  where
    actual_kind = typeKind ty

387 388 389 390 391
-- | 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 _@

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

Austin Seipp's avatar
Austin Seipp committed
407
{-
408 409
Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
410
Technically
411 412 413 414
            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
415
-}
416 417 418 419 420 421 422 423

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
424

425 426
          | MustBeMonoType  -- Monotype regardless of flags

427 428 429 430 431 432

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")
433 434 435 436 437 438 439 440 441 442 443

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

----------------------------------------
444
check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
445 446
-- 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
447
--
448 449 450
-- Rank is allowed rank for function args
-- Rank 0 means no for-alls anywhere

451
check_type env ctxt rank ty
452
  | not (null tvs && null theta)
453 454
  = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
        ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
Austin Seipp's avatar
Austin Seipp committed
455
                -- Reject e.g. (Maybe (?x::Int => Int)),
456
                -- with a decent error message
457

458
        ; check_valid_theta env' SigmaCtxt theta
459 460 461
                -- Allow     type T = ?x::Int => Int -> Int
                -- but not   type T = ?x::Int

462
        ; check_type env' ctxt rank tau      -- Allow foralls to right of arrow
463
        ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
464 465
                   (forAllEscapeErr env' ty tau_kind)
        }
466 467
  where
    (tvs, theta, tau) = tcSplitSigmaTy ty
468
    tau_kind          = typeKind tau
469
    (env', _)         = tidyTyCoVarBndrs env tvs
470 471 472 473 474

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

475
check_type _ _ _ (TyVarTy _) = return ()
476

Simon Peyton Jones's avatar
Simon Peyton Jones committed
477
check_type env ctxt rank (FunTy arg_ty res_ty)
478 479
  = do  { check_type env ctxt arg_rank arg_ty
        ; check_type env ctxt res_rank res_ty }
480 481 482
  where
    (arg_rank, res_rank) = funArgResRank rank

483 484 485
check_type env ctxt rank (AppTy ty1 ty2)
  = do  { check_arg_type env ctxt rank ty1
        ; check_arg_type env ctxt rank ty2 }
486

487
check_type env ctxt rank ty@(TyConApp tc tys)
488
  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
489 490 491 492 493
  = 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 ()
494

495
check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
496

497
check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
498 499

----------------------------------------
500
check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
501
                 -> TyCon -> [KindOrType] -> TcM ()
502
-- Used for type synonyms and type synonym families,
Austin Seipp's avatar
Austin Seipp committed
503
-- which must be saturated,
504
-- but not data families, which need not be saturated
505
check_syn_tc_app env ctxt rank ty tc tys
506
  | tys `lengthAtLeast` tc_arity   -- Saturated
507 508 509 510 511 512 513
       -- 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]
514
        ; liberal <- xoptM LangExt.LiberalTypeSynonyms
515
        ; if not liberal || isTypeFamilyTyCon tc then
516
                -- For H98 and synonym families, do check the type args
517
                mapM_ check_arg tys
518 519

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

Austin Seipp's avatar
Austin Seipp committed
524
  | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in
525
                      -- GHCi :kind commands; see Trac #7586
526
  = mapM_ check_arg tys
527 528

  | otherwise
529
  = failWithTc (tyConArityErr tc tys)
530 531
  where
    tc_arity  = tyConArity tc
532 533
    check_arg | isTypeFamilyTyCon tc = check_arg_type  env ctxt rank
              | otherwise            = check_type      env ctxt synArgMonoType
Austin Seipp's avatar
Austin Seipp committed
534

535
----------------------------------------
536
check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
537
                -> [KindOrType] -> TcM ()
538
check_ubx_tuple env ctxt ty tys
539
  = do  { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
540
        ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
541

542
        ; impred <- xoptM LangExt.ImpredicativeTypes
543 544 545 546
        ; 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
547
        ; mapM_ (check_type env ctxt rank') tys }
Austin Seipp's avatar
Austin Seipp committed
548

549
----------------------------------------
550
check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
551 552 553 554 555
-- 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
556
--
557 558 559 560 561 562 563 564 565 566 567 568
-- 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

569 570 571
check_arg_type _ _ _ (CoercionTy {}) = return ()

check_arg_type env ctxt rank ty
572
  = do  { impred <- xoptM LangExt.ImpredicativeTypes
573 574 575 576
        ; 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
577
                        -- Make sure that MustBeMonoType is propagated,
578 579 580 581
                        -- 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!

582
        ; check_type env ctxt rank' ty }
583 584

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

599 600 601 602 603 604 605 606
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 ]) )

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

Austin Seipp's avatar
Austin Seipp committed
610
{-
611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639
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
640 641
************************************************************************
*                                                                      *
642
\subsection{Checking a theta or source type}
Austin Seipp's avatar
Austin Seipp committed
643 644
*                                                                      *
************************************************************************
645

646 647 648 649 650 651 652 653
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
654 655
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
656
applying the instance decl would show up two uses of ?x.  Trac #8912.
Austin Seipp's avatar
Austin Seipp committed
657
-}
658

659
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
Edward Z. Yang's avatar
Edward Z. Yang committed
660
-- Assumes argument is fully zonked
661
checkValidTheta ctxt theta
niteria's avatar
niteria committed
662
  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
663 664
       ; addErrCtxtM (checkThetaCtxt ctxt theta) $
         check_valid_theta env ctxt theta }
665 666

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

-------------------------
683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
{- 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.
-}

707
check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
708
-- Check the validity of a predicate in a signature
709
-- See Note [Validity checking for constraints]
710
check_pred_ty env dflags ctxt pred
711
  = do { check_type env SigmaCtxt constraintMonoType pred
712
       ; check_pred_help False env dflags ctxt pred }
713 714

check_pred_help :: Bool    -- True <=> under a type synonym
715
                -> TidyEnv
716 717
                -> DynFlags -> UserTypeCtxt
                -> PredType -> TcM ()
718
check_pred_help under_syn env dflags ctxt pred
Ben Gamari's avatar
Ben Gamari committed
719
  | Just pred' <- tcView pred  -- Switch on under_syn when going under a
720
                                 -- synonym (Trac #9838, yuk)
721
  = check_pred_help True env dflags ctxt pred'
722
  | otherwise
723
  = case splitTyConApp_maybe pred of
724 725
      Just (tc, tys)
        | isTupleTyCon tc
726 727 728 729 730 731 732
        -> check_tuple_pred under_syn env dflags ctxt pred tys
           -- NB: this equality check must come first, because (~) is a class,
           -- too.
        | tc `hasKey` heqTyConKey ||
          tc `hasKey` eqTyConKey ||
          tc `hasKey` eqPrimTyConKey
        -> check_eq_pred env dflags pred tc tys
733
        | Just cls <- tyConClass_maybe tc
734 735
        -> check_class_pred env dflags ctxt pred cls tys  -- Includes Coercible
      _ -> check_irred_pred under_syn env dflags ctxt pred
736

737 738
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
739 740
  =         -- Equational constraints are valid in all contexts if type
            -- families are permitted
741
    do { checkTc (tys `lengthIs` tyConArity tc) (tyConArityErr tc tys)
742 743
       ; checkTcM (xopt LangExt.TypeFamilies dflags
                   || xopt LangExt.GADTs dflags)
744
                  (eqPredTyErr env pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
745

746 747
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
748
  = do { -- See Note [ConstraintKinds in predicates]
749
         checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
750 751
                  (predTupleErr env pred)
       ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
752 753
    -- This case will not normally be executed because without
    -- -XConstraintKinds tuple types are only kind-checked as *
754

755 756
check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
check_irred_pred under_syn env dflags ctxt pred
757
    -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
758 759 760 761 762
    -- 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)
763
        failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
764
                                && hasTyVarHead pred)
765
                  (predIrredErr env pred)
766 767 768

         -- Make sure it is OK to have an irred pred in this context
         -- See Note [Irreducible predicates in superclasses]
769
       ; failIfTcM (is_superclass ctxt
770
                    && not (xopt LangExt.UndecidableInstances dflags)
771 772
                    && has_tyfun_head pred)
                   (predSuperClassErr env pred) }
773
  where
774 775 776 777 778
    is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
    has_tyfun_head ty
      = case tcSplitTyConApp_maybe ty of
          Just (tc, _) -> isTypeFamilyTyCon tc
          Nothing      -> False
779 780 781 782 783 784 785 786 787 788 789 790 791

{- 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
792
Allowing type-family calls in class superclasses is somewhat dangerous
793 794 795 796 797 798 799 800
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
801
solved to add+canonicalise another (Foo a) constraint.  -}
802 803

-------------------------
804 805
check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
check_class_pred env dflags ctxt pred cls tys
806
  | isIPClass cls
807
  = do { check_arity
808
       ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
809

810
  | otherwise
811
  = do { check_arity
812 813
       ; warn_simp <- woptM Opt_WarnSimplifiableClassConstraints
       ; when warn_simp check_simplifiable_class_constraint
814
       ; checkTcM arg_tys_ok (predTyVarErr env pred) }
815
  where
816
    check_arity = checkTc (tys `lengthIs` classArity cls)
817
                          (tyConArityErr (classTyCon cls) tys)
818 819

    -- Check the arguments of a class constraint
820 821
    flexible_contexts = xopt LangExt.FlexibleContexts     dflags
    undecidable_ok    = xopt LangExt.UndecidableInstances dflags
822 823
    arg_tys_ok = case ctxt of
        SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
824
        InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
825 826
                                -- Further checks on head and theta
                                -- in checkInstTermination
827
        _            -> checkValidClsArgs flexible_contexts cls tys
828

829 830
    -- See Note [Simplifiable given constraints]
    check_simplifiable_class_constraint
831 832
       | xopt LangExt.MonoLocalBinds dflags
       = return ()
833 834 835
       | DataTyCtxt {} <- ctxt   -- Don't do this check for the "stupid theta"
       = return ()               -- of a data type declaration
       | otherwise
836 837 838 839 840 841 842 843
       = 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, _)
844 845 846
     = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
                 2 (text "matches an instance declaration")
            , ppr match
847 848
            , hang (text "This makes type inference for inner bindings fragile;")
                 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
849 850

{- Note [Simplifiable given constraints]
851
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
852 853 854
A type signature like
   f :: Eq [(a,b)] => a -> b
is very fragile, for reasons described at length in TcInteract
855 856 857 858 859 860 861
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
862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882
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!
883 884
-}

885 886 887
-------------------------
okIPCtxt :: UserTypeCtxt -> Bool
  -- See Note [Implicit parameters in instance decls]
888 889 890 891 892 893 894 895 896 897 898 899 900
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
901
okIPCtxt (PatSynCtxt {})        = True
902 903
okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
                                         -- Trac #11466
904

905 906 907
okIPCtxt (ClassSCCtxt {})  = False
okIPCtxt (InstDeclCtxt {}) = False
okIPCtxt (SpecInstCtxt {}) = False
908 909
okIPCtxt (RuleSigCtxt {})  = False
okIPCtxt DefaultDeclCtxt   = False
910

Austin Seipp's avatar
Austin Seipp committed
911
{-
912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929
Note [Kind polymorphic type classes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
MultiParam check:

    class C f where...   -- C :: forall k. k -> Constraint
    instance C Maybe where...

  The dictionary gets type [C * Maybe] even if it's not a MultiParam
  type class.

Flexibility check:

    class C f where...   -- C :: forall k. k -> Constraint
    data D a = D a
    instance C D where

  The dictionary gets type [C * (D *)]. IA0_TODO it should be
  generalized actually.
Austin Seipp's avatar
Austin Seipp committed
930 931
-}

932 933 934
checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt ctxt theta env
  = return ( env
935 936
           , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
                  , text "While checking" <+> pprUserTypeCtxt ctxt ] )
937 938 939 940

eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
eqPredTyErr  env pred
  = ( env
941 942
    , text "Illegal equational constraint" <+> ppr_tidy env pred $$
      parens (text "Use GADTs or TypeFamilies to permit this") )
943 944
predTupleErr env pred
  = ( env
945
    , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
946 947 948
         2 (parens constraintKindsMsg) )
predIrredErr env pred
  = ( env
949
    , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
950 951 952
         2 (parens constraintKindsMsg) )
predSuperClassErr env pred
  = ( env
953 954
    , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
            <+> text "in a superclass context")
955 956
         2 (parens undecidableMsg) )

957 958 959 960 961 962 963 964 965 966 967
predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
predTyVarErr env pred
  = (env
    , vcat [ hang (text "Non type-variable argument")
                2 (text "in the constraint:" <+> ppr_tidy env pred)
           , parens (text "Use FlexibleContexts to permit this") ])

badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
badIPPred env pred
  = ( env
    , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
968 969 970 971

constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintSynErr env kind
  = ( env
972
    , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
973 974 975 976 977
         2 (parens constraintKindsMsg) )

dupPredWarn :: TidyEnv -> [[PredType]] -> (TidyEnv, SDoc)
dupPredWarn env dups
  = ( env
978 979 980 981
    , text "Duplicate constraint" <> plural primaryDups <> text ":"
      <+> pprWithCommas (ppr_tidy env) primaryDups )
  where
    primaryDups = map head dups
982

983 984
tyConArityErr :: TyCon -> [TcType] -> SDoc
-- For type-constructor arity errors, be careful to report
985 986
-- the number of /visible/ arguments required and supplied,
-- ignoring the /invisible/ arguments, which the user does not see.
987 988
-- (e.g. Trac #10516)
tyConArityErr tc tks
989
  = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
990 991
             tc_type_arity tc_type_args
  where
992
    vis_tks = filterOutInvisibleTypes tc tks
993 994 995

    -- tc_type_arity = number of *type* args expected
    -- tc_type_args  = number of *type* args encountered
996
    tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
997
    tc_type_args  = length vis_tks
998

999
arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1000
arityErr what name n m
1001
  = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
Austin Seipp's avatar
Austin Seipp committed
1002
           n_arguments <> comma, text "but has been given",
1003 1004
           if m==0 then text "none" else int m]
    where