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

6 7
{-# LANGUAGE CPP #-}

8 9
module TcValidity (
  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
Austin Seipp's avatar
Austin Seipp committed
10
  expectedKindInCtxt,
11
  checkValidTheta, checkValidFamPats,
12
  checkValidInstance, validDerivPred,
Jan Stolarek's avatar
Jan Stolarek committed
13
  checkInstTermination,
14
  ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
15
  checkValidTyFamEqn,
16
  checkConsistentFamInst,
17 18 19 20 21 22
  arityErr, badATErr
  ) where

#include "HsVersions.h"

-- friends:
23
import TcUnify    ( tcSubType_NC )
24
import TcSimplify ( simplifyAmbiguityCheck )
25 26 27
import TypeRep
import TcType
import TcMType
28
import TysWiredIn ( coercibleClass, eqTyCon )
29
import PrelNames
30 31 32 33 34 35 36 37 38 39 40
import Type
import Unify( tcMatchTyX )
import Kind
import CoAxiom
import Class
import TyCon

-- others:
import HsSyn            -- HsType
import TcRnMonad        -- TcType, amongst others
import FunDeps
Jan Stolarek's avatar
Jan Stolarek committed
41 42 43
import FamInstEnv  ( isDominatedBy, injectiveBranches,
                     InjectivityCheckResult(..) )
import FamInst     ( makeInjectivityErrors )
44 45 46 47 48 49 50 51 52 53 54 55
import Name
import VarEnv
import VarSet
import ErrUtils
import DynFlags
import Util
import ListSetOps
import SrcLoc
import Outputable
import FastString

import Control.Monad
Icelandjack's avatar
Icelandjack committed
56
import Data.Maybe
57 58
import Data.List        ( (\\) )

Austin Seipp's avatar
Austin Seipp committed
59 60 61
{-
************************************************************************
*                                                                      *
62
          Checking for ambiguity
Austin Seipp's avatar
Austin Seipp committed
63 64
*                                                                      *
************************************************************************
65 66 67 68 69 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 120 121 122 123 124 125 126 127 128 129 130 131 132 133

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

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

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

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
188
-}
189 190 191

checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity ctxt ty
192 193 194 195 196
  | GhciCtxt <- ctxt    -- Allow ambiguous types in GHCi's :kind command
  = return ()           -- E.g.   type family T a :: *  -- T :: forall k. k -> *
                        -- Then :k T should work in GHCi, not complain that
                        -- (T k) is ambiguous!

197
  | InfSigCtxt {} <- ctxt  -- See Note [Validity of inferred types] in TcBinds
Austin Seipp's avatar
Austin Seipp committed
198
  = return ()
199

200
  | otherwise
201
  = do { traceTc "Ambiguity check for" (ppr ty)
202 203
       ; let free_tkvs = varSetElemsKvsFirst (closeOverKinds (tyVarsOfType ty))
       ; (subst, _tvs) <- tcInstSkolTyVars free_tkvs
204
       ; let ty' = substTy subst ty
205 206 207
              -- The type might have free TyVars, esp when the ambiguity check
              -- happens during a call to checkValidType,
              -- so we skolemise them as TcTyVars.
208
              -- Tiresome; but the type inference engine expects TcTyVars
209 210 211
              -- NB: The free tyvar might be (a::k), so k is also free
              --     and we must skolemise it as well. Hence closeOverKinds.
              --     (Trac #9222)
212 213

         -- Solve the constraints eagerly because an ambiguous type
214
         -- can cause a cascade of further errors.  Since the free
215
         -- tyvars are skolemised, we can safely use tcSimplifyTop
216 217
       ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
                            captureConstraints $
218
                            tcSubType_NC ctxt ty' ty'
219 220 221 222 223
       ; whenNoErrs $  -- only run the simplifier if we have a clean
                       -- environment. Otherwise we might trip.
                       -- example: indexed-types/should_fail/BadSock
                       -- fails in DEBUG mode without this
         simplifyAmbiguityCheck ty wanted
224

225
       ; traceTc "Done ambiguity check for" (ppr ty) }
226
 where
227 228
   mk_msg ty tidy_env
     = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
229 230
          ; (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty
          ; return (tidy_env', mk_msg tidy_ty $$ ppWhen (not allow_ambiguous) ambig_msg) }
231
     where
232
       mk_msg ty = pprSigCtxt ctxt (ptext (sLit "the ambiguity check for")) (ppr ty)
233
       ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
234

235 236 237 238 239 240 241 242 243 244

checkUserTypeError :: Type -> TcM ()
checkUserTypeError = check
  where
  check ty
    | Just (_,msg) <- isUserErrorTy ty = failWithTc (pprUserTypeErrorTy msg)
    | Just (_,ts)  <- splitTyConApp_maybe ty  = mapM_ check ts
    | Just (t1,t2) <- splitAppTy_maybe ty     = check t1 >> check t2
    | otherwise                               = return ()

Austin Seipp's avatar
Austin Seipp committed
245 246 247
{-
************************************************************************
*                                                                      *
248
          Checking validity of a user-defined type
Austin Seipp's avatar
Austin Seipp committed
249 250
*                                                                      *
************************************************************************
251 252

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

Austin Seipp's avatar
Austin Seipp committed
260
One thing we check for is 'rank'.
261 262 263 264 265 266 267 268 269 270 271

        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
272 273

Another thing is to check that type synonyms are saturated.
274 275 276 277
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
278
-}
279 280 281 282

checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
-- Not used for instance decls; checkValidInstance instead
Austin Seipp's avatar
Austin Seipp committed
283
checkValidType ctxt ty
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
       ; rankn_flag  <- xoptM Opt_RankNTypes
       ; 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
300
                 PatSigCtxt     -> rank0
301 302 303
                 RuleSigCtxt _  -> rank1
                 TySynCtxt _    -> rank0

304 305 306 307
                 ExprSigCtxt     -> rank1
                 FunSigCtxt {}   -> rank1
                 InfSigCtxt _    -> ArbitraryRank        -- Inferred type
                 ConArgCtxt _    -> rank1 -- We are given the type of the entire
308 309 310 311 312 313 314 315 316 317 318 319
                                         -- constructor, hence rank 1

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

        -- Check the internal validity of the type itself
       ; check_type ctxt rank ty

320 321 322
        -- Check that the thing has kind Type, and is lifted if necessary.
        -- Do this *after* check_type, because we can't usefully take
        -- the kind of an ill-formed type such as (a~Int)
323
       ; check_kind ctxt ty
324

325 326
       ; checkUserTypeError ty

327
       -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
328 329
       -- NB: this will happen even for monotypes, but that should be cheap;
       --     and there may be nested foralls for the subtype test to examine
330 331
       ; checkAmbiguity ctxt ty

332
       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
333 334 335 336 337 338 339 340 341

checkValidMonoType :: Type -> TcM ()
checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty


check_kind :: UserTypeCtxt -> TcType -> TcM ()
-- Check that the type's kind is acceptable for the context
check_kind ctxt ty
  | TySynCtxt {} <- ctxt
342
  , returnsConstraintKind actual_kind
343
  = do { ck <- xoptM Opt_ConstraintKinds
344 345 346 347 348
       ; if ck
         then  when (isConstraintKind actual_kind)
                    (do { dflags <- getDynFlags
                        ; check_pred_ty dflags ctxt ty })
         else addErrTc (constraintSynErr actual_kind) }
349 350 351 352 353 354 355 356 357 358 359 360

  | Just k <- expectedKindInCtxt ctxt
  = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)

  | otherwise
  = return ()   -- Any kind will do
  where
    actual_kind = typeKind ty

-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
361 362 363 364 365 366 367 368 369 370
expectedKindInCtxt (TySynCtxt _)   = Nothing -- Any kind will do
expectedKindInCtxt ThBrackCtxt     = Nothing
expectedKindInCtxt GhciCtxt        = Nothing
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in TcEnv
expectedKindInCtxt DefaultDeclCtxt = Nothing
expectedKindInCtxt (ForSigCtxt _)  = Just liftedTypeKind
expectedKindInCtxt InstDeclCtxt    = Just constraintKind
expectedKindInCtxt SpecInstCtxt    = Just constraintKind
expectedKindInCtxt _               = Just openTypeKind
371

Austin Seipp's avatar
Austin Seipp committed
372
{-
373 374
Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
375
Technically
376 377 378 379
            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
380
-}
381 382 383 384 385 386 387 388

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
389

390 391 392
          | MustBeMonoType  -- Monotype regardless of flags

rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
393
rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))
394
tyConArgMonoType = MonoType (ptext (sLit "GHC doesn't yet support impredicative polymorphism"))
395
synArgMonoType   = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418

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

----------------------------------------
check_mono_type :: UserTypeCtxt -> Rank
                -> KindOrType -> TcM () -- No foralls anywhere
                                        -- No unlifted types of any kind
check_mono_type ctxt rank ty
  | isKind ty = return ()  -- IA0_NOTE: Do we need to check kinds?
  | otherwise
   = do { check_type ctxt rank ty
        ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }

check_type :: UserTypeCtxt -> Rank -> Type -> TcM ()
-- 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
419
--
420 421 422 423 424 425
-- Rank is allowed rank for function args
-- Rank 0 means no for-alls anywhere

check_type ctxt rank ty
  | not (null tvs && null theta)
  = do  { checkTc (forAllAllowed rank) (forAllTyErr rank ty)
Austin Seipp's avatar
Austin Seipp committed
426
                -- Reject e.g. (Maybe (?x::Int => Int)),
427
                -- with a decent error message
428 429 430 431 432

        ; check_valid_theta SigmaCtxt theta
                -- Allow     type T = ?x::Int => Int -> Int
                -- but not   type T = ?x::Int

433
        ; check_type ctxt rank tau }      -- Allow foralls to right of arrow
434 435
  where
    (tvs, theta, tau) = tcSplitSigmaTy ty
Austin Seipp's avatar
Austin Seipp committed
436

437 438 439 440 441 442 443 444 445 446 447 448 449
check_type _ _ (TyVarTy _) = return ()

check_type ctxt rank (FunTy arg_ty res_ty)
  = do  { check_type ctxt arg_rank arg_ty
        ; check_type ctxt res_rank res_ty }
  where
    (arg_rank, res_rank) = funArgResRank rank

check_type ctxt rank (AppTy ty1 ty2)
  = do  { check_arg_type ctxt rank ty1
        ; check_arg_type ctxt rank ty2 }

check_type ctxt rank ty@(TyConApp tc tys)
450 451
  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
  = check_syn_tc_app ctxt rank ty tc tys
452 453 454 455 456 457 458 459
  | isUnboxedTupleTyCon tc = check_ubx_tuple  ctxt      ty    tys
  | otherwise              = mapM_ (check_arg_type ctxt rank) tys

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

check_type _ _ ty = pprPanic "check_type" (ppr ty)

----------------------------------------
460
check_syn_tc_app :: UserTypeCtxt -> Rank -> KindOrType
461
                 -> TyCon -> [KindOrType] -> TcM ()
462
-- Used for type synonyms and type synonym families,
Austin Seipp's avatar
Austin Seipp committed
463
-- which must be saturated,
464
-- but not data families, which need not be saturated
465
check_syn_tc_app ctxt rank ty tc tys
466
  | tc_arity <= length tys   -- Saturated
467 468 469 470 471 472 473
       -- 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]
474
        ; liberal <- xoptM Opt_LiberalTypeSynonyms
475
        ; if not liberal || isTypeFamilyTyCon tc then
476
                -- For H98 and synonym families, do check the type args
477
                mapM_ check_arg tys
478 479

          else  -- In the liberal case (only for closed syns), expand then check
Austin Seipp's avatar
Austin Seipp committed
480 481
          case tcView ty of
             Just ty' -> check_type ctxt rank ty'
482 483
             Nothing  -> pprPanic "check_tau_type" (ppr ty)  }

Austin Seipp's avatar
Austin Seipp committed
484
  | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in
485
                      -- GHCi :kind commands; see Trac #7586
486
  = mapM_ check_arg tys
487 488

  | otherwise
489
  = failWithTc (tyConArityErr tc tys)
490 491
  where
    tc_arity  = tyConArity tc
492 493
    check_arg | isTypeFamilyTyCon tc = check_arg_type  ctxt rank
              | otherwise            = check_mono_type ctxt synArgMonoType
Austin Seipp's avatar
Austin Seipp committed
494

495
----------------------------------------
Austin Seipp's avatar
Austin Seipp committed
496
check_ubx_tuple :: UserTypeCtxt -> KindOrType
497 498
                -> [KindOrType] -> TcM ()
check_ubx_tuple ctxt ty tys
499
  = do  { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
500
        ; checkTc ub_tuples_allowed (ubxArgTyErr ty)
501

Austin Seipp's avatar
Austin Seipp committed
502
        ; impred <- xoptM Opt_ImpredicativeTypes
503 504 505 506 507
        ; 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
        ; mapM_ (check_type ctxt rank') tys }
Austin Seipp's avatar
Austin Seipp committed
508

509 510 511 512 513 514 515
----------------------------------------
check_arg_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM ()
-- 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
516
--
517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536
-- 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

check_arg_type ctxt rank ty
  | isKind ty = return ()  -- IA0_NOTE: Do we need to check a kind?
  | otherwise
  = do  { impred <- xoptM Opt_ImpredicativeTypes
        ; 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
537
                        -- Make sure that MustBeMonoType is propagated,
538 539 540 541 542 543
                        -- 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!

        ; check_type ctxt rank' ty
        ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
Austin Seipp's avatar
Austin Seipp committed
544
             -- NB the isUnLiftedType test also checks for
545 546 547 548 549 550
             --    T State#
             -- where there is an illegal partial application of State# (which has
             -- kind * -> #); see Note [The kind invariant] in TypeRep

----------------------------------------
forAllTyErr :: Rank -> Type -> SDoc
Austin Seipp's avatar
Austin Seipp committed
551
forAllTyErr rank ty
552 553 554 555
   = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
          , suggestion ]
  where
    suggestion = case rank of
556
                   LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")
557
                   MonoType d     -> d
558
                   _              -> Outputable.empty -- Polytype is always illegal
559 560 561 562 563 564 565 566

unliftedArgErr, ubxArgTyErr :: Type -> SDoc
unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]

kindErr :: Kind -> SDoc
kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]

Austin Seipp's avatar
Austin Seipp committed
567
{-
568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
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
597 598
************************************************************************
*                                                                      *
599
\subsection{Checking a theta or source type}
Austin Seipp's avatar
Austin Seipp committed
600 601
*                                                                      *
************************************************************************
602

603 604 605 606 607 608 609 610
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
611 612
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
613
applying the instance decl would show up two uses of ?x.  Trac #8912.
Austin Seipp's avatar
Austin Seipp committed
614
-}
615

616
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
617
checkValidTheta ctxt theta
618 619 620 621 622 623 624 625 626 627
  = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)

-------------------------
check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM ()
check_valid_theta _ []
  = return ()
check_valid_theta ctxt theta
  = do { dflags <- getDynFlags
       ; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
                 notNull dups) (dupPredWarn dups)
628
       ; traceTc "check_valid_theta" (ppr theta)
629 630 631 632 633 634 635
       ; mapM_ (check_pred_ty dflags ctxt) theta }
  where
    (_,dups) = removeDups cmpPred theta

-------------------------
check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
-- Check the validity of a predicate in a signature
636
-- Do not look through any type synonyms; any constraint kinded
637
-- type synonyms have been checked at their definition site
638
-- C.f. Trac #9838
639 640

check_pred_ty dflags ctxt pred
641 642 643 644 645 646 647
  = do { checkValidMonoType pred
       ; check_pred_help False dflags ctxt pred }

check_pred_help :: Bool    -- True <=> under a type synonym
                -> DynFlags -> UserTypeCtxt
                -> PredType -> TcM ()
check_pred_help under_syn dflags ctxt pred
648 649
  | Just pred' <- coreView pred  -- Switch on under_syn when going under a
                                 -- synonym (Trac #9838, yuk)
650
  = check_pred_help True dflags ctxt pred'
651
  | otherwise
652
  = case splitTyConApp_maybe pred of
653 654 655 656 657 658 659
      Just (tc, tys)
        | isTupleTyCon tc
        -> check_tuple_pred under_syn dflags ctxt pred tys
        | Just cls <- tyConClass_maybe tc
        -> check_class_pred dflags ctxt pred cls tys  -- Includes Coercible
        | tc `hasKey` eqTyConKey
        -> check_eq_pred dflags pred tys
660 661 662 663
      _ -> check_irred_pred under_syn dflags ctxt pred

check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
check_eq_pred dflags pred tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
664 665
  =         -- Equational constraints are valid in all contexts if type
            -- families are permitted
666 667
    do { checkTc (length tys == 3)
                 (tyConArityErr eqTyCon tys)
668 669
       ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
                 (eqPredTyErr pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
670

671 672
check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
check_tuple_pred under_syn dflags ctxt pred ts
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
673
  = do { -- See Note [ConstraintKinds in predicates]
674
         checkTc (under_syn || xopt Opt_ConstraintKinds dflags)
675
                 (predTupleErr pred)
676 677 678
       ; mapM_ (check_pred_help under_syn dflags ctxt) ts }
    -- This case will not normally be executed because without
    -- -XConstraintKinds tuple types are only kind-checked as *
679

680 681
check_irred_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
check_irred_pred under_syn dflags ctxt pred
682
    -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
683 684 685 686 687
    -- 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)
688 689 690
        failIfTc (not under_syn && not (xopt Opt_ConstraintKinds dflags)
                                && hasTyVarHead pred)
                 (predIrredErr pred)
691 692 693

         -- Make sure it is OK to have an irred pred in this context
         -- See Note [Irreducible predicates in superclasses]
694 695 696 697
       ; failIfTc (is_superclass ctxt
                   && not (xopt Opt_UndecidableInstances dflags)
                   && has_tyfun_head pred)
                  (predSuperClassErr pred) }
698
  where
699 700 701 702 703
    is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
    has_tyfun_head ty
      = case tcSplitTyConApp_maybe ty of
          Just (tc, _) -> isTypeFamilyTyCon tc
          Nothing      -> False
704 705 706 707 708 709 710 711 712 713 714 715 716

{- 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
717
Allowing type-family calls in class superclasses is somewhat dangerous
718 719 720 721 722 723 724 725
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
726
solved to add+canonicalise another (Foo a) constraint.  -}
727 728

-------------------------
729 730 731
check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
check_class_pred dflags ctxt pred cls tys
  | isIPClass cls
732 733
  = do { check_arity
       ; checkTc (okIPCtxt ctxt) (badIPPred pred) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
734

735
  | otherwise
736
  = do { check_arity
737 738
       ; checkTc arg_tys_ok (predTyVarErr pred) }
  where
739 740
    check_arity = checkTc (classArity cls == length tys)
                          (tyConArityErr (classTyCon cls) tys)
741 742
    flexible_contexts = xopt Opt_FlexibleContexts     dflags
    undecidable_ok    = xopt Opt_UndecidableInstances dflags
743

744 745 746 747 748 749
    arg_tys_ok = case ctxt of
        SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
        InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys
                                -- Further checks on head and theta
                                -- in checkInstTermination
        _            -> checkValidClsArgs flexible_contexts tys
750 751 752 753

-------------------------
okIPCtxt :: UserTypeCtxt -> Bool
  -- See Note [Implicit parameters in instance decls]
754 755 756 757 758 759 760 761 762 763 764 765
okIPCtxt (FunSigCtxt {})    = True
okIPCtxt (InfSigCtxt {})    = True
okIPCtxt ExprSigCtxt        = 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
766
okIPCtxt (PatSynCtxt {})    = True
767

768 769 770
okIPCtxt (ClassSCCtxt {})  = False
okIPCtxt (InstDeclCtxt {}) = False
okIPCtxt (SpecInstCtxt {}) = False
771 772 773
okIPCtxt (TySynCtxt {})    = False
okIPCtxt (RuleSigCtxt {})  = False
okIPCtxt DefaultDeclCtxt   = False
774 775 776

badIPPred :: PredType -> SDoc
badIPPred pred = ptext (sLit "Illegal implicit parameter") <+> quotes (ppr pred)
777

Austin Seipp's avatar
Austin Seipp committed
778
{-
779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796
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
797 798
-}

799 800 801 802 803
checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc
checkThetaCtxt ctxt theta
  = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
          ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]

804 805 806
eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predSuperClassErr :: PredType -> SDoc
eqPredTyErr  pred  = vcat [ ptext (sLit "Illegal equational constraint") <+> pprType pred
                          , parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) ]
807 808 809
predTyVarErr pred  = vcat [ hang (ptext (sLit "Non type-variable argument"))
                               2 (ptext (sLit "in the constraint:") <+> pprType pred)
                          , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
810
predTupleErr pred  = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
811
                        2 (parens constraintKindsMsg)
812
predIrredErr pred  = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
813
                        2 (parens constraintKindsMsg)
814 815 816 817
predSuperClassErr pred
  = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
          <+> ptext (sLit "in a superclass context"))
       2 (parens undecidableMsg)
818 819 820

constraintSynErr :: Type -> SDoc
constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))
821
                           2 (parens constraintKindsMsg)
822 823 824 825

dupPredWarn :: [[PredType]] -> SDoc
dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)

826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844
tyConArityErr :: TyCon -> [TcType] -> SDoc
-- For type-constructor arity errors, be careful to report
-- the number of /type/ arguments required and supplied,
-- ignoring the /kind/ arguments, which the user does not see.
-- (e.g. Trac #10516)
tyConArityErr tc tks
  = arityErr (tyConFlavour tc) (tyConName tc)
             tc_type_arity tc_type_args
  where
    tvs = tyConTyVars tc

    kbs :: [Bool]  -- True for a Type arg, false for a Kind arg
    kbs = map isTypeVar tvs

    -- tc_type_arity = number of *type* args expected
    -- tc_type_args  = number of *type* args encountered
    tc_type_arity = count id kbs
    tc_type_args  = count (id . fst) (kbs `zip` tks)

845
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
846 847
arityErr what name n m
  = hsep [ ptext (sLit "The") <+> text what, quotes (ppr name), ptext (sLit "should have"),
Austin Seipp's avatar
Austin Seipp committed
848
           n_arguments <> comma, text "but has been given",
849 850 851 852 853 854
           if m==0 then text "none" else int m]
    where
        n_arguments | n == 0 = ptext (sLit "no arguments")
                    | n == 1 = ptext (sLit "1 argument")
                    | True   = hsep [int n, ptext (sLit "arguments")]

Austin Seipp's avatar
Austin Seipp committed
855 856 857
{-
************************************************************************
*                                                                      *
858
\subsection{Checking for a decent instance head type}
Austin Seipp's avatar
Austin Seipp committed
859 860
*                                                                      *
************************************************************************
861 862 863 864 865 866 867 868 869

@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
870
-}
871 872 873 874 875

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

876 877 878
       ; checkTc (clas `notElem` abstractClasses)
                 (instTypeErr clas cls_args abstract_class_msg)

Austin Seipp's avatar
Austin Seipp committed
879
           -- Check language restrictions;
880 881 882 883 884 885 886 887 888 889
           -- but not for SPECIALISE isntance pragmas
       ; let ty_args = dropWhile isKind cls_args
       ; unless spec_inst_prag $
         do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
                       all tcInstHeadTyNotSynonym ty_args)
                 (instTypeErr clas cls_args head_type_synonym_msg)
            ; checkTc (xopt Opt_FlexibleInstances dflags ||
                       all tcInstHeadTyAppAllTyVars ty_args)
                 (instTypeErr clas cls_args head_type_args_tyvars_msg)
            ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
890 891 892
                       length ty_args == 1 ||  -- Only count type arguments
                       (xopt Opt_NullaryTypeClasses dflags &&
                        null ty_args))
893 894 895 896 897 898
                 (instTypeErr clas cls_args head_one_type_msg) }

         -- May not contain type family applications
       ; mapM_ checkTyFamFreeness ty_args

       ; mapM_ checkValidMonoType ty_args
Austin Seipp's avatar
Austin Seipp committed
899 900
        -- For now, I only allow tau-types (not polytypes) in
        -- the head of an instance decl.
901 902 903 904 905 906 907 908 909 910 911
        --      E.g.  instance C (forall a. a->a) is rejected
        -- One could imagine generalising that, but I'm not sure
        -- what all the consequences might be
       }

  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." $$
912
                text "Use TypeSynonymInstances if you want to disable this.")
913 914 915 916 917

    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.",
918
                text "Use FlexibleInstances if you want to disable this."])
919 920 921

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

924 925 926 927
    abstract_class_msg =
                text "The class is abstract, manual instances are not permitted."

abstractClasses :: [ Class ]
Joachim Breitner's avatar
Joachim Breitner committed
928
abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]
929

930 931
instTypeErr :: Class -> [Type] -> SDoc -> SDoc
instTypeErr cls tys msg
932 933
  = hang (hang (ptext (sLit "Illegal instance declaration for"))
             2 (quotes (pprClassPred cls tys)))
934 935
       2 msg

Simon Peyton Jones's avatar
Simon Peyton Jones committed
936 937 938
{- Note [Valid 'deriving' predicate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
validDerivPred checks for OK 'deriving' context.  See Note [Exotic
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
939
derived instance contexts] in TcDeriv.  However the predicate is
940 941
here because it uses sizeTypes, fvTypes.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958
It checks for three things

  * No repeated variables (hasNoDups fvs)

  * No type constructors.  This is done by comparing
        sizeTypes tys == length (fvTypes tys)
    sizeTypes counts variables and constructors; fvTypes returns variables.
    So if they are the same, there must be no constructors.  But there
    might be applications thus (f (g x)).

  * Also check for a bizarre corner case, when the derived instance decl
    would look like
       instance C a b => D (T a) where ...
    Note that 'b' isn't a parameter of T.  This gives rise to all sorts of
    problems; in particular, it's hard to compare solutions for equality
    when finding the fixpoint, and that means the inferContext loop does
   not converge.  See Trac #5287.
Austin Seipp's avatar
Austin Seipp committed
959
-}
960 961

validDerivPred :: TyVarSet -> PredType -> Bool
Simon Peyton Jones's avatar
Simon Peyton Jones committed
962
-- See Note [Valid 'deriving' predicate]
963 964
validDerivPred tv_set pred
  = case classifyPredType pred of
965 966 967
       ClassPred _ tys -> check_tys tys
       EqPred {}       -> False  -- reject equality constraints
       _               -> True   -- Non-class predicates are ok
968
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
969
    check_tys tys = hasNoDups fvs
970
                    && sizeTypes tys == fromIntegral (length fvs)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
971
                    && all (`elemVarSet` tv_set) fvs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
972 973
                  where
                    fvs = fvTypes tys
974

Austin Seipp's avatar
Austin Seipp committed
975 976 977
{-
************************************************************************
*                                                                      *
978
\subsection{Checking instance for termination}
Austin Seipp's avatar
Austin Seipp committed
979 980 981
*                                                                      *
************************************************************************
-}
982 983 984 985

checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
                   -> TcM ([TyVar], ThetaType, Class, [Type])
checkValidInstance ctxt hs_type ty
986 987 988
  | Just (clas,inst_tys) <- getClassPredTys_maybe tau
  , inst_tys `lengthIs` classArity clas
  = do  { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
989 990 991 992 993 994
        ; checkValidTheta ctxt theta

        -- The Termination and Coverate Conditions
        -- Check that instance inference will terminate (if we care)
        -- For Haskell 98 this will already have been done by checkValidTheta,
        -- but as we may be using other extensions we need to check.
Austin Seipp's avatar
Austin Seipp committed
995 996
        --
        -- Note that the Termination Condition is *more conservative* than
997 998 999 1000 1001
        -- the checkAmbiguity test we do on other type signatures
        --   e.g.  Bar a => Bar Int is ambiguous, but it also fails
        --   the termination condition, because 'a' appears more often
        --   in the constraint than in the head
        ; undecidable_ok <- xoptM Opt_UndecidableInstances
Austin Seipp's avatar
Austin Seipp committed
1002
        ; if undecidable_ok
1003 1004 1005 1006
          then checkAmbiguity ctxt ty
          else checkInstTermination inst_tys theta

        ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1007 1008
            IsValid  -> return ()   -- Check succeeded
            NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1009

Austin Seipp's avatar
Austin Seipp committed
1010 1011 1012
        ; return (tvs, theta, clas, inst_tys) }

  | otherwise
1013
  = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
1014
  where
1015
    (tvs, theta, tau) = tcSplitSigmaTy ty
1016 1017 1018

        -- The location of the "head" of the instance
    head_loc = case hs_type of
thomasw's avatar
thomasw committed
1019 1020
                 L _ (HsForAllTy _ _ _ _ (L loc _)) -> loc
                 L loc _                            -> loc
1021

Austin Seipp's avatar
Austin Seipp committed
1022
{-
1023 1024 1025
Note [Paterson conditions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Termination test: the so-called "Paterson conditions" (see Section 5 of
Jan Stolarek's avatar
Jan Stolarek committed
1026
"Understanding functional dependencies via Constraint Handling Rules,
1027 1028 1029 1030 1031 1032 1033
JFP Jan 2007).

We check that each assertion in the context satisfies:
 (1) no variable has more occurrences in the assertion than in the head, and
 (2) the assertion has fewer constructors and variables (taken together
     and counting repetitions) than the head.
This is only needed with -fglasgow-exts, as Haskell 98 restrictions
Austin Seipp's avatar
Austin Seipp committed
1034
(which have already been checked) guarantee termination.
1035

Austin Seipp's avatar
Austin Seipp committed
1036
The underlying idea is that
1037 1038 1039

    for any ground substitution, each assertion in the
    context has fewer type constructors than the head.
Austin Seipp's avatar
Austin Seipp committed
1040
-}
1041 1042 1043 1044

checkInstTermination :: [TcType] -> ThetaType -> TcM ()
-- See Note [Paterson conditions]
checkInstTermination tys theta
1045
  = check_preds theta
1046
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1047 1048
   head_fvs  = fvTypes tys
   head_size = sizeTypes tys
1049 1050 1051 1052 1053

   check_preds :: [PredType] -> TcM ()
   check_preds preds = mapM_ check preds

   check :: PredType -> TcM ()
Austin Seipp's avatar
Austin Seipp committed
1054
   check pred
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1055 1056 1057 1058 1059 1060 1061 1062
     = case classifyPredType pred of
         EqPred {}    -> return ()  -- See Trac #4200.
         IrredPred {} -> check2 pred (sizeType pred)
         ClassPred cls tys
           | isIPClass cls
           -> return ()  -- You can't get to class predicates from implicit params

           | isCTupleClass cls  -- Look inside tuple predicates; Trac #8359