TcValidity.hs 79.4 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     ( ClsInst, lookupInstEnv, isOverlappable )
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 60
import BasicTypes
import Module
61
import Unique      ( mkAlphaTyVarUnique )
62
import qualified GHC.LanguageExtensions as LangExt
63 64 65 66

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

Austin Seipp's avatar
Austin Seipp committed
67 68 69
{-
************************************************************************
*                                                                      *
70
          Checking for ambiguity
Austin Seipp's avatar
Austin Seipp committed
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 120 121 122 123 124 125 126 127 128 129 130 131

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
unambiguous. See Note [Impedence matching] in TcBinds.

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

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

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

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

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

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

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

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

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

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


253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
{- 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
273 274
************************************************************************
*                                                                      *
275
          Checking validity of a user-defined type
Austin Seipp's avatar
Austin Seipp committed
276 277
*                                                                      *
************************************************************************
278 279

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

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

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

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

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

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

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

353
       ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
354

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

358 359
       ; checkUserTypeError ty

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

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

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

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

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

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

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

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

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
425

426 427
          | MustBeMonoType  -- Monotype regardless of flags

428 429 430 431 432 433

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

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

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

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

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

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

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

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

478
check_type env ctxt rank (FunTy arg_ty res_ty)
479 480
  = do  { check_type env ctxt arg_rank arg_ty
        ; check_type env ctxt res_rank res_ty }
481 482 483
  where
    (arg_rank, res_rank) = funArgResRank rank

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

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

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

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

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

          else  -- In the liberal case (only for closed syns), expand then check
521
          case coreView ty of
522
             Just ty' -> check_type env ctxt rank ty'
523 524
             Nothing  -> pprPanic "check_tau_type" (ppr ty)  }

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

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

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

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

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

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

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

583
        ; check_type env ctxt rank' ty }
584 585

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

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

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

Austin Seipp's avatar
Austin Seipp committed
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 640
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
641 642
************************************************************************
*                                                                      *
643
\subsection{Checking a theta or source type}
Austin Seipp's avatar
Austin Seipp committed
644 645
*                                                                      *
************************************************************************
646

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

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

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

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

check_pred_help :: Bool    -- True <=> under a type synonym
716
                -> TidyEnv
717 718
                -> DynFlags -> UserTypeCtxt
                -> PredType -> TcM ()
719
check_pred_help under_syn env dflags ctxt pred
720 721
  | Just pred' <- coreView pred  -- Switch on under_syn when going under a
                                 -- synonym (Trac #9838, yuk)
722
  = check_pred_help True env dflags ctxt pred'
723
  | otherwise
724
  = case splitTyConApp_maybe pred of
725 726
      Just (tc, tys)
        | isTupleTyCon tc
727 728 729 730 731 732 733
        -> 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
734
        | Just cls <- tyConClass_maybe tc
735 736
        -> check_class_pred env dflags ctxt pred cls tys  -- Includes Coercible
      _ -> check_irred_pred under_syn env dflags ctxt pred
737

738 739
check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
check_eq_pred env dflags pred tc tys
740 741
  =         -- Equational constraints are valid in all contexts if type
            -- families are permitted
742
    do { checkTc (length tys == tyConArity tc) (tyConArityErr tc tys)
743 744
       ; checkTcM (xopt LangExt.TypeFamilies dflags
                   || xopt LangExt.GADTs dflags)
745
                  (eqPredTyErr env pred) }
746

747 748
check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
check_tuple_pred under_syn env dflags ctxt pred ts
749
  = do { -- See Note [ConstraintKinds in predicates]
750
         checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
751 752
                  (predTupleErr env pred)
       ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
753 754
    -- This case will not normally be executed because without
    -- -XConstraintKinds tuple types are only kind-checked as *
755

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

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

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

-------------------------
805 806
check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
check_class_pred env dflags ctxt pred cls tys
807
  | isIPClass cls
808
  = do { check_arity
809
       ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
810

811
  | otherwise
812
  = do { check_arity
813 814
       ; check_simplifiable_class_constraint
       ; checkTcM arg_tys_ok (predTyVarErr env pred) }
815
  where
816 817
    check_arity = checkTc (classArity cls == length tys)
                          (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 836 837 838 839 840 841 842 843 844 845 846 847 848
       | DataTyCtxt {} <- ctxt   -- Don't do this check for the "stupid theta"
       = return ()               -- of a data type declaration
       | otherwise
       = do { instEnvs <- tcGetInstEnvs
            ; let (matches, _, _) = lookupInstEnv False instEnvs cls tys
                  bad_matches = [ inst | (inst,_) <- matches
                                       , not (isOverlappable inst) ]
            ; warnIf (Reason Opt_WarnSimplifiableClassConstraints)
                     (not (null bad_matches))
                     (simplifiable_constraint_warn bad_matches) }

    simplifiable_constraint_warn :: [ClsInst] -> SDoc
    simplifiable_constraint_warn (match : _)
     = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
                 2 (text "matches an instance declaration")
            , ppr match
849 850
            , hang (text "This makes type inference for inner bindings fragile;")
                 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
851 852 853 854 855 856 857
    simplifiable_constraint_warn [] = pprPanic "check_class_pred" (ppr pred)

{- Note [Simplifiable given constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A type signature like
   f :: Eq [(a,b)] => a -> b
is very fragile, for reasons described at length in TcInteract
858 859 860 861 862 863 864 865 866 867
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
that case the warning discourages uses from writing simplifiable class
constraints, at least unless the top-level instance is explicitly
declared as OVERLAPPABLE.
868 869
-}

870 871 872
-------------------------
okIPCtxt :: UserTypeCtxt -> Bool
  -- See Note [Implicit parameters in instance decls]
873 874 875 876 877 878 879 880 881 882 883 884 885
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
886
okIPCtxt (PatSynCtxt {})        = True
887 888
okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
                                         -- Trac #11466
889

890 891 892
okIPCtxt (ClassSCCtxt {})  = False
okIPCtxt (InstDeclCtxt {}) = False
okIPCtxt (SpecInstCtxt {}) = False
893 894
okIPCtxt (RuleSigCtxt {})  = False
okIPCtxt DefaultDeclCtxt   = False
895

Austin Seipp's avatar
Austin Seipp committed
896
{-
897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914
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
915 916
-}

917 918 919
checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt ctxt theta env
  = return ( env
920 921
           , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
                  , text "While checking" <+> pprUserTypeCtxt ctxt ] )
922 923 924 925

eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
eqPredTyErr  env pred
  = ( env
926 927
    , text "Illegal equational constraint" <+> ppr_tidy env pred $$
      parens (text "Use GADTs or TypeFamilies to permit this") )
928 929
predTupleErr env pred
  = ( env
930
    , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
931 932 933
         2 (parens constraintKindsMsg) )
predIrredErr env pred
  = ( env
934
    , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
935 936 937
         2 (parens constraintKindsMsg) )
predSuperClassErr env pred
  = ( env
938 939
    , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
            <+> text "in a superclass context")
940 941
         2 (parens undecidableMsg) )

942 943 944 945 946 947 948 949 950 951 952
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) )
953 954 955 956

constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintSynErr env kind
  = ( env
957
    , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
958 959 960 961 962
         2 (parens constraintKindsMsg) )

dupPredWarn :: TidyEnv -> [[PredType]] -> (TidyEnv, SDoc)
dupPredWarn env dups
  = ( env
963 964 965 966
    , text "Duplicate constraint" <> plural primaryDups <> text ":"
      <+> pprWithCommas (ppr_tidy env) primaryDups )
  where
    primaryDups = map head dups
967

968 969
tyConArityErr :: TyCon -> [TcType] -> SDoc
-- For type-constructor arity errors, be careful to report
970 971
-- the number of /visible/ arguments required and supplied,
-- ignoring the /invisible/ arguments, which the user does not see.
972 973 974 975 976
-- (e.g. Trac #10516)
tyConArityErr tc tks
  = arityErr (tyConFlavour tc) (tyConName tc)
             tc_type_arity tc_type_args
  where
977
    vis_tks = filterOutInvisibleTypes tc tks
978 979 980

    -- tc_type_arity = number of *type* args expected
    -- tc_type_args  = number of *type* args encountered
981
    tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
982
    tc_type_args  = length vis_tks
983

984
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
985
arityErr what name n m
986
  = hsep [ text "The" <+> text what, quotes (ppr name), text "should have",
Austin Seipp's avatar
Austin Seipp committed
987
           n_arguments <> comma, text "but has been given",
988 989
           if m==0 then text "none" else int m]
    where
990 991 992
        n_arguments | n == 0 = text "no arguments"
                    | n == 1 = text "1 argument"
                    | True   = hsep [int n, text "arguments"]
993

Austin Seipp's avatar
Austin Seipp committed
994 995 996
{-
************************************************************************
*                                                                      *
997
\subsection{Checking for a decent instance head type}
Austin Seipp's avatar
Austin Seipp committed
998 999
*                                                                      *
************************************************************************
1000 1001 1002 1003 1004 1005 1006 1007 1008

@checkValidInstHead@ checks the type {\em and} its syntactic constraints:
it must normally look like: @instance Foo (Tycon a b c ...) ...@

The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
flag is on, or (2)~the instance is imported (they must have been
compiled elsewhere). In these cases, we let them go through anyway.

We can also have instances for functions: @instance Foo (a -> b) ...@.
Austin Seipp's avatar
Austin Seipp committed
1009
-}
1010 1011 1012 1013 1014

checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead ctxt clas cls_args
  = do { dflags <- getDynFlags

1015 1016 1017
       ; mod <- getModule
       ; checkTc (getUnique clas `notElem` abstractClassKeys ||
                  nameModule (getName clas) == mod)
1018 1019
                 (instTypeErr clas cls_args abstract_class_msg)

1020 1021 1022
       ; when (clas `hasKey` hasFieldClassNameKey) $
             checkHasFieldInst clas cls_args

Austin Seipp's avatar
Austin Seipp committed
1023
           -- Check language restrictions;
Gabor Greif's avatar
Gabor Greif committed
1024
           -- but not for SPECIALISE instance pragmas
1025
       ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1026
       ; unless spec_inst_prag $
1027
         do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
1028 1029
                       all tcInstHeadTyNotSynonym ty_args)
                 (instTypeErr clas cls_args head_type_synonym_msg)
1030
            ; checkTc (xopt LangExt.FlexibleInstances dflags ||
1031 1032
                       all tcInstHeadTyAppAllTyVars ty_args)
                 (instTypeErr clas cls_args head_type_args_tyvars_msg)
1033
            ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
1034
                       length ty_args == 1 ||  -- Only count type arguments
1035
                       (xopt LangExt.NullaryTypeClasses dflags &&
1036
                        null ty_args))
1037 1038
                 (instTypeErr clas cls_args head_one_type_msg) }

1039
       ; mapM_ checkValidTypePat ty_args }
1040 1041 1042 1043 1044 1045
  where
    spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }

    head_type_synonym_msg = parens (
                text "All instance types must be of the form (T t1 ... tn)" $$
                text "where T is not a synonym." $$
1046
                text "Use TypeSynonymInstances if you want to disable this.")
1047 1048 1049 1050 1051

    head_type_args_tyvars_msg = parens (vcat [
                text "All instance types must be of the form (T a1 ... an)",
                text "where a1 ... an are *distinct type variables*,",
                text "and each type variable appears at most once in the instance head.",
1052
                text "Use FlexibleInstances if you want to disable this."])
1053 1054 1055

    head_one_type_msg = parens (
                text "Only one type can be given in an instance head." $$
1056
                text "Use MultiParamTypeClasses if you want to allow more, or zero.")
1057

1058
    abstract_class_msg =
1059
                text "Manual instances of this class are not permitted."
1060

1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094
tcInstHeadTyNotSynonym :: Type -> Bool
-- Used in Haskell-98 mode, for the argument types of an instance head
-- These must not be type synonyms, but everywhere else type synonyms
-- are transparent, so we need a special function here
tcInstHeadTyNotSynonym ty
  = case ty of  -- Do not use splitTyConApp,
                -- because that expands synonyms!
        TyConApp tc _ -> not (isTypeSynonymTyCon tc)
        _ -> True

tcInstHeadTyAppAllTyVars :: Type -> Bool
-- Used in Haskell-98 mode, for the argument types of an instance head
-- These must be a constructor applied to type variable arguments.
-- But we allow kind instantiations.
tcInstHeadTyAppAllTyVars ty
  | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
  = ok (filterOutInvisibleTypes tc tys)  -- avoid kinds

  | otherwise
  = False
  where
        -- Check that all the types are type variables,
        -- and that each is distinct
    ok tys = equalLength tvs tys && hasNoDups tvs
           where
             tvs = mapMaybe tcGetTyVar_maybe tys

dropCasts :: Type -> Type
-- See Note [Casts during validity checking]
-- This function can turn a well-kinded type into an ill-kinded
-- one, so I've kept it local to this module
-- To consider: drop only UnivCo(HoleProv) casts
dropCasts (CastTy ty _)     = dropCasts ty
dropCasts (AppTy t1 t2)     = mkAppTy (dropCasts t1) (dropCasts t2)
1095
dropCasts (FunTy t1 t2)     = mkFunTy (dropCasts t1) (dropCasts t2)
1096 1097 1098 1099
dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
dropCasts (ForAllTy b ty)   = ForAllTy (dropCastsB b) (dropCasts ty)
dropCasts ty                = ty  -- LitTy, TyVarTy, CoercionTy

1100 1101
dropCastsB :: TyVarBinder -> TyVarBinder
dropCastsB b = b   -- Don't bother in the kind of a forall
1102

1103 1104 1105 1106 1107
abstractClassKeys :: [Unique]
abstractClassKeys = [ heqTyConKey
                    , eqTyConKey
                    , coercibleTyConKey
                    ] -- See Note [Equality class instances]
1108

1109 1110
instTypeErr :: Class -> [Type] -> SDoc -> SDoc
instTypeErr cls tys msg
1111
  = hang (hang (text "Illegal instance declaration for")
1112
             2 (quotes (pprClassPred cls tys)))
1113 1114
       2 msg

1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135
-- | See Note [Validity checking of HasField instances]
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
  case splitTyConApp_maybe r_ty of
    Nothing -> whoops (text "Record data type must be specified")
    Just (tc, _)
      | isFamilyTyCon tc
                  -> whoops (text "Record data type may not be a data family")
      | otherwise -> case isStrLitTy x_ty of
       Just lbl
         | isJust (lookupTyConFieldLabel lbl tc)
                     -> whoops (ppr tc <+> text "already has a field"
                                       <+> quotes (ppr lbl))
         | otherwise -> return ()
       Nothing
         | null (tyConFieldLabels tc) -> return ()
         | otherwise -> whoops (ppr tc <+> text "has fields")
  where
    whoops = addErrTc . instTypeErr cls tys
checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)

1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150
{- Note [Casts during validity checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the (bogus)
     instance Eq Char#
We elaborate to  'Eq (Char# |> UnivCo(hole))'  where the hole is an
insoluble equality constraint for * ~ #.  We'll report the insoluble
constraint separately, but we don't want to *also* complain that Eq is
not applied to a type constructor.  So we look gaily look through
CastTys here.

Another example:  Eq (Either a).  Then we actually get a cast in
the middle:
   Eq ((Either |> g) a)


1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170
Note [Validity checking of HasField instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The HasField class has magic constraint solving behaviour (see Note
[HasField instances] in TcInteract).  However, we permit users to
declare their own instances, provided they do not clash with the
built-in behaviour.  In particular, we forbid:

  1. `HasField _ r _` where r is a variable

  2. `HasField _ (T ...) _` if T is a data family
     (because it might have fields introduced later)

  3. `HasField x (T ...) _` where x is a variable,
      if T has any fields at all

  4. `HasField "foo" (T ...) _` if T has a "foo" field

The usual functional dependency checks also apply.


1171 1172
Note [Valid 'deriving' predicate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1173
validDerivPred checks for OK 'deriving' context.  See Note [Exotic
1174
derived instance contexts] in TcDeriv.  However the predicate is
1175 1176
here because it uses sizeTypes, fvTypes.

1177 1178 1179 1180 1181 1182 1183 1184 1185 1186
It checks for three things

  * No repeated variables (hasNoDups fvs)

  * No type constructors.  This is done by comparing
        sizeTypes tys == length (fvTypes tys)