2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Monadic type operations
8 This module contains monadic operations over types that contain
13 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
15 --------------------------------
16 -- Creating new mutable type variables
18 newFlexiTyVarTy, -- Kind -> TcM TcType
19 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
20 newKindVar, newKindVars,
21 lookupTcTyVar, LookupTyVarResult(..),
22 newMetaTyVar, readMetaTyVar, writeMetaTyVar,
24 --------------------------------
25 -- Boxy type variables
26 newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
28 --------------------------------
29 -- Creating new coercion variables
32 --------------------------------
34 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
35 tcInstSigTyVars, zonkSigTyVar,
36 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
37 tcSkolSigType, tcSkolSigTyVars,
39 --------------------------------
40 -- Checking type validity
41 Rank, UserTypeCtxt(..), checkValidType,
42 SourceTyCtxt(..), checkValidTheta, checkFreeness,
43 checkValidInstHead, checkValidInstance, checkAmbiguity,
47 --------------------------------
49 zonkType, zonkTcPredType,
50 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
51 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
52 zonkTcKindToKind, zonkTcKind,
54 readKindVar, writeKindVar
58 #include "HsVersions.h"
71 import TcRnMonad -- TcType, amongst others
81 import Control.Monad ( when )
82 import Data.List ( (\\) )
86 %************************************************************************
88 Instantiation in general
90 %************************************************************************
93 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
94 -> TcType -- Type to instantiate
95 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
96 tcInstType inst_tyvars ty
97 = case tcSplitForAllTys ty of
98 ([], rho) -> let -- There may be overloading despite no type variables;
99 -- (?x :: Int) => Int -> Int
100 (theta, tau) = tcSplitPhiTy rho
102 return ([], theta, tau)
104 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
106 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
107 -- Either the tyvars are freshly made, by inst_tyvars,
108 -- or (in the call from tcSkolSigType) any nested foralls
109 -- have different binders. Either way, zipTopTvSubst is ok
111 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
112 ; return (tyvars', theta, tau) }
116 %************************************************************************
120 %************************************************************************
123 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
125 = do { us <- newUniqueSupply
126 ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
128 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
130 newKindVar :: TcM TcKind
131 newKindVar = do { uniq <- newUnique
132 ; ref <- newMutVar Flexi
133 ; return (mkTyVarTy (mkKindVar uniq ref)) }
135 newKindVars :: Int -> TcM [TcKind]
136 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
140 %************************************************************************
142 SkolemTvs (immutable)
144 %************************************************************************
147 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
148 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
150 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
151 -- Instantiate a type signature with skolem constants, but
152 -- do *not* give them fresh names, because we want the name to
153 -- be in the type environment -- it is lexically scoped.
154 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
156 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
157 -- Make skolem constants, but do *not* give them new names, as above
158 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
161 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
162 -- Instantiate a type with fresh skolem constants
163 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
165 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
166 tcInstSkolTyVar info tyvar
167 = do { uniq <- newUnique
168 ; let name = setNameUnique (tyVarName tyvar) uniq
169 kind = tyVarKind tyvar
170 ; return (mkSkolTyVar name kind info) }
172 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
173 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
177 %************************************************************************
179 MetaTvs (meta type variables; mutable)
181 %************************************************************************
184 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
185 -- Make a new meta tyvar out of thin air
186 newMetaTyVar box_info kind
187 = do { uniq <- newUnique
188 ; ref <- newMutVar Flexi ;
189 ; let name = mkSysTvName uniq fs
190 fs = case box_info of
193 SigTv _ -> FSLIT("a")
194 -- We give BoxTv and TauTv the same string, because
195 -- otherwise we get user-visible differences in error
196 -- messages, which are confusing. If you want to see
197 -- the box_info of each tyvar, use -dppr-debug
198 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
200 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
201 -- Make a new meta tyvar whose Name and Kind
202 -- come from an existing TyVar
203 instMetaTyVar box_info tyvar
204 = do { uniq <- newUnique
205 ; ref <- newMutVar Flexi ;
206 ; let name = setNameUnique (tyVarName tyvar) uniq
207 kind = tyVarKind tyvar
208 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
210 readMetaTyVar :: TyVar -> TcM MetaDetails
211 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
212 readMutVar (metaTvRef tyvar)
214 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
216 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
218 writeMetaTyVar tyvar ty
219 | not (isMetaTyVar tyvar)
220 = pprTrace "writeMetaTyVar" (ppr tyvar) $
224 = ASSERT( isMetaTyVar tyvar )
225 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
226 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
227 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
235 %************************************************************************
239 %************************************************************************
242 newFlexiTyVar :: Kind -> TcM TcTyVar
243 newFlexiTyVar kind = newMetaTyVar TauTv kind
245 newFlexiTyVarTy :: Kind -> TcM TcType
247 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
248 returnM (TyVarTy tc_tyvar)
250 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
251 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
253 tcInstTyVar :: TyVar -> TcM TcTyVar
254 -- Instantiate with a META type variable
255 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
257 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
258 -- Instantiate with META type variables
260 = do { tc_tvs <- mapM tcInstTyVar tyvars
261 ; let tys = mkTyVarTys tc_tvs
262 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
263 -- Since the tyvars are freshly made,
264 -- they cannot possibly be captured by
265 -- any existing for-alls. Hence zipTopTvSubst
269 %************************************************************************
273 %************************************************************************
276 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
277 -- Instantiate with meta SigTvs
278 tcInstSigTyVars skol_info tyvars
279 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
281 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
283 | isSkolemTyVar sig_tv
284 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
286 = ASSERT( isSigTyVar sig_tv )
287 do { ty <- zonkTcTyVar sig_tv
288 ; return (tcGetTyVar "zonkSigTyVar" ty) }
289 -- 'ty' is bound to be a type variable, because SigTvs
290 -- can only be unified with type variables
294 %************************************************************************
298 %************************************************************************
301 newBoxyTyVar :: Kind -> TcM BoxyTyVar
302 newBoxyTyVar kind = newMetaTyVar BoxTv kind
304 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
305 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
307 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
308 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
310 readFilledBox :: BoxyTyVar -> TcM TcType
311 -- Read the contents of the box, which should be filled in by now
312 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
313 do { cts <- readMetaTyVar box_tv
315 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
316 Indirect ty -> return ty }
318 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
319 -- Instantiate with a BOXY type variable
320 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
324 %************************************************************************
326 \subsection{Putting and getting mutable type variables}
328 %************************************************************************
330 But it's more fun to short out indirections on the way: If this
331 version returns a TyVar, then that TyVar is unbound. If it returns
332 any other type, then there might be bound TyVars embedded inside it.
334 We return Nothing iff the original box was unbound.
337 data LookupTyVarResult -- The result of a lookupTcTyVar call
338 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
341 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
343 = ASSERT( isTcTyVar tyvar )
345 SkolemTv _ -> return (DoneTv details)
346 MetaTv _ ref -> do { meta_details <- readMutVar ref
347 ; case meta_details of
348 Indirect ty -> return (IndirectTv ty)
349 Flexi -> return (DoneTv details) }
351 details = tcTyVarDetails tyvar
354 -- gaw 2004 We aren't shorting anything out anymore, at least for now
356 | not (isTcTyVar tyvar)
357 = pprTrace "getTcTyVar" (ppr tyvar) $
358 returnM (Just (mkTyVarTy tyvar))
361 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
362 readMetaTyVar tyvar `thenM` \ maybe_ty ->
364 Just ty -> short_out ty `thenM` \ ty' ->
365 writeMetaTyVar tyvar (Just ty') `thenM_`
368 Nothing -> returnM Nothing
370 short_out :: TcType -> TcM TcType
371 short_out ty@(TyVarTy tyvar)
372 | not (isTcTyVar tyvar)
376 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
378 Just ty' -> short_out ty' `thenM` \ ty' ->
379 writeMetaTyVar tyvar (Just ty') `thenM_`
384 short_out other_ty = returnM other_ty
389 %************************************************************************
391 \subsection{Zonking -- the exernal interfaces}
393 %************************************************************************
395 ----------------- Type variables
398 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
399 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
401 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
402 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
403 returnM (tyVarsOfTypes tys)
405 zonkTcTyVar :: TcTyVar -> TcM TcType
406 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
407 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
410 ----------------- Types
413 zonkTcType :: TcType -> TcM TcType
414 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
416 zonkTcTypes :: [TcType] -> TcM [TcType]
417 zonkTcTypes tys = mappM zonkTcType tys
419 zonkTcClassConstraints cts = mappM zonk cts
420 where zonk (clas, tys)
421 = zonkTcTypes tys `thenM` \ new_tys ->
422 returnM (clas, new_tys)
424 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
425 zonkTcThetaType theta = mappM zonkTcPredType theta
427 zonkTcPredType :: TcPredType -> TcM TcPredType
428 zonkTcPredType (ClassP c ts)
429 = zonkTcTypes ts `thenM` \ new_ts ->
430 returnM (ClassP c new_ts)
431 zonkTcPredType (IParam n t)
432 = zonkTcType t `thenM` \ new_t ->
433 returnM (IParam n new_t)
434 zonkTcPredType (EqPred t1 t2)
435 = zonkTcType t1 `thenM` \ new_t1 ->
436 zonkTcType t2 `thenM` \ new_t2 ->
437 returnM (EqPred new_t1 new_t2)
440 ------------------- These ...ToType, ...ToKind versions
441 are used at the end of type checking
444 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
445 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
446 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
447 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
448 -- The meta tyvar is updated to point to the new regular TyVar. Now any
449 -- bound occurences of the original type variable will get zonked to
450 -- the immutable version.
452 -- We leave skolem TyVars alone; they are immutable.
453 zonkQuantifiedTyVar tv
454 | isSkolemTyVar tv = return tv
455 -- It might be a skolem type variable,
456 -- for example from a user type signature
458 | otherwise -- It's a meta-type-variable
459 = do { details <- readMetaTyVar tv
461 -- Create the new, frozen, regular type variable
462 ; let final_kind = defaultKind (tyVarKind tv)
463 final_tv = mkTyVar (tyVarName tv) final_kind
465 -- Bind the meta tyvar to the new tyvar
467 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
469 -- [Sept 04] I don't think this should happen
470 -- See note [Silly Type Synonym]
472 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
474 -- Return the new tyvar
478 [Silly Type Synonyms]
481 type C u a = u -- Note 'a' unused
483 foo :: (forall a. C u a -> C u a) -> u
487 bar = foo (\t -> t + t)
489 * From the (\t -> t+t) we get type {Num d} => d -> d
492 * Now unify with type of foo's arg, and we get:
493 {Num (C d a)} => C d a -> C d a
496 * Now abstract over the 'a', but float out the Num (C d a) constraint
497 because it does not 'really' mention a. (see exactTyVarsOfType)
498 The arg to foo becomes
501 * So we get a dict binding for Num (C d a), which is zonked to give
503 [Note Sept 04: now that we are zonking quantified type variables
504 on construction, the 'a' will be frozen as a regular tyvar on
505 quantification, so the floated dict will still have type (C d a).
506 Which renders this whole note moot; happily!]
508 * Then the /\a abstraction has a zonked 'a' in it.
510 All very silly. I think its harmless to ignore the problem. We'll end up with
511 a /\a in the final result but all the occurrences of a will be zonked to ()
514 %************************************************************************
516 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
518 %* For internal use only! *
520 %************************************************************************
523 -- For unbound, mutable tyvars, zonkType uses the function given to it
524 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
525 -- type variable and zonks the kind too
527 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
528 -- see zonkTcType, and zonkTcTypeToType
531 zonkType unbound_var_fn ty
534 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
536 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
537 returnM (TyConApp tc tys')
539 go (PredTy p) = go_pred p `thenM` \ p' ->
542 go (FunTy arg res) = go arg `thenM` \ arg' ->
543 go res `thenM` \ res' ->
544 returnM (FunTy arg' res')
546 go (AppTy fun arg) = go fun `thenM` \ fun' ->
547 go arg `thenM` \ arg' ->
548 returnM (mkAppTy fun' arg')
549 -- NB the mkAppTy; we might have instantiated a
550 -- type variable to a type constructor, so we need
551 -- to pull the TyConApp to the top.
553 -- The two interesting cases!
554 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
555 | otherwise = return (TyVarTy tyvar)
556 -- Ordinary (non Tc) tyvars occur inside quantified types
558 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
559 go ty `thenM` \ ty' ->
560 returnM (ForAllTy tyvar ty')
562 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
563 returnM (ClassP c tys')
564 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
565 returnM (IParam n ty')
566 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
567 go ty2 `thenM` \ ty2' ->
568 returnM (EqPred ty1' ty2')
570 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
571 -> TcTyVar -> TcM TcType
572 zonk_tc_tyvar unbound_var_fn tyvar
573 | not (isMetaTyVar tyvar) -- Skolems
574 = returnM (TyVarTy tyvar)
576 | otherwise -- Mutables
577 = do { cts <- readMetaTyVar tyvar
579 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
580 Indirect ty -> zonkType unbound_var_fn ty }
585 %************************************************************************
589 %************************************************************************
592 readKindVar :: KindVar -> TcM (MetaDetails)
593 writeKindVar :: KindVar -> TcKind -> TcM ()
594 readKindVar kv = readMutVar (kindVarRef kv)
595 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
598 zonkTcKind :: TcKind -> TcM TcKind
599 zonkTcKind k = zonkTcType k
602 zonkTcKindToKind :: TcKind -> TcM Kind
603 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
604 -- Haskell specifies that * is to be used, so we follow that.
605 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
608 %************************************************************************
610 \subsection{Checking a user type}
612 %************************************************************************
614 When dealing with a user-written type, we first translate it from an HsType
615 to a Type, performing kind checking, and then check various things that should
616 be true about it. We don't want to perform these checks at the same time
617 as the initial translation because (a) they are unnecessary for interface-file
618 types and (b) when checking a mutually recursive group of type and class decls,
619 we can't "look" at the tycons/classes yet. Also, the checks are are rather
620 diverse, and used to really mess up the other code.
622 One thing we check for is 'rank'.
624 Rank 0: monotypes (no foralls)
625 Rank 1: foralls at the front only, Rank 0 inside
626 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
628 basic ::= tyvar | T basic ... basic
630 r2 ::= forall tvs. cxt => r2a
631 r2a ::= r1 -> r2a | basic
632 r1 ::= forall tvs. cxt => r0
633 r0 ::= r0 -> r0 | basic
635 Another thing is to check that type synonyms are saturated.
636 This might not necessarily show up in kind checking.
638 data T k = MkT (k Int)
643 checkValidType :: UserTypeCtxt -> Type -> TcM ()
644 -- Checks that the type is valid for the given context
645 checkValidType ctxt ty
646 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
647 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
649 rank | gla_exts = Arbitrary
651 = case ctxt of -- Haskell 98
653 LamPatSigCtxt -> Rank 0
654 BindPatSigCtxt -> Rank 0
655 DefaultDeclCtxt-> Rank 0
657 TySynCtxt _ -> Rank 0
658 ExprSigCtxt -> Rank 1
659 FunSigCtxt _ -> Rank 1
660 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
661 -- constructor, hence rank 1
662 ForSigCtxt _ -> Rank 1
663 RuleSigCtxt _ -> Rank 1
664 SpecInstCtxt -> Rank 1
666 actual_kind = typeKind ty
668 kind_ok = case ctxt of
669 TySynCtxt _ -> True -- Any kind will do
670 ResSigCtxt -> isSubOpenTypeKind actual_kind
671 ExprSigCtxt -> isSubOpenTypeKind actual_kind
672 GenPatCtxt -> isLiftedTypeKind actual_kind
673 ForSigCtxt _ -> isLiftedTypeKind actual_kind
674 other -> isSubArgTypeKind actual_kind
676 ubx_tup | not gla_exts = UT_NotOk
677 | otherwise = case ctxt of
681 -- Unboxed tuples ok in function results,
682 -- but for type synonyms we allow them even at
685 -- Check that the thing has kind Type, and is lifted if necessary
686 checkTc kind_ok (kindErr actual_kind) `thenM_`
688 -- Check the internal validity of the type itself
689 check_poly_type rank ubx_tup ty `thenM_`
691 traceTc (text "checkValidType done" <+> ppr ty)
696 data Rank = Rank Int | Arbitrary
698 decRank :: Rank -> Rank
699 decRank Arbitrary = Arbitrary
700 decRank (Rank n) = Rank (n-1)
702 ----------------------------------------
703 data UbxTupFlag = UT_Ok | UT_NotOk
704 -- The "Ok" version means "ok if -fglasgow-exts is on"
706 ----------------------------------------
707 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
708 check_poly_type (Rank 0) ubx_tup ty
709 = check_tau_type (Rank 0) ubx_tup ty
711 check_poly_type rank ubx_tup ty
712 | null tvs && null theta
713 = check_tau_type rank ubx_tup ty
715 = do { check_valid_theta SigmaCtxt theta
716 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
717 ; checkFreeness tvs theta
718 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
720 (tvs, theta, tau) = tcSplitSigmaTy ty
722 ----------------------------------------
723 check_arg_type :: Type -> TcM ()
724 -- The sort of type that can instantiate a type variable,
725 -- or be the argument of a type constructor.
726 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
727 -- Other unboxed types are very occasionally allowed as type
728 -- arguments depending on the kind of the type constructor
730 -- For example, we want to reject things like:
732 -- instance Ord a => Ord (forall s. T s a)
734 -- g :: T s (forall b.b)
736 -- NB: unboxed tuples can have polymorphic or unboxed args.
737 -- This happens in the workers for functions returning
738 -- product types with polymorphic components.
739 -- But not in user code.
740 -- Anyway, they are dealt with by a special case in check_tau_type
743 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
744 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
746 ----------------------------------------
747 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
748 -- Rank is allowed rank for function args
749 -- No foralls otherwise
751 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
752 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
753 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
755 -- Naked PredTys don't usually show up, but they can as a result of
756 -- {-# SPECIALISE instance Ord Char #-}
757 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
758 -- are handled, but the quick thing is just to permit PredTys here.
759 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
760 check_pred_ty dflags TypeCtxt sty
762 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
763 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
764 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
765 check_poly_type rank UT_Ok res_ty
767 check_tau_type rank ubx_tup (AppTy ty1 ty2)
768 = check_arg_type ty1 `thenM_` check_arg_type ty2
770 check_tau_type rank ubx_tup (NoteTy other_note ty)
771 = check_tau_type rank ubx_tup ty
773 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
775 = do { -- It's OK to have an *over-applied* type synonym
776 -- data Tree a b = ...
777 -- type Foo a = Tree [a]
778 -- f :: Foo a b -> ...
780 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
781 Nothing -> failWithTc arity_msg
783 ; gla_exts <- doptM Opt_GlasgowExts
785 -- If -fglasgow-exts then don't check the type arguments
786 -- This allows us to instantiate a synonym defn with a
787 -- for-all type, or with a partially-applied type synonym.
788 -- e.g. type T a b = a
791 -- Here, T is partially applied, so it's illegal in H98.
792 -- But if you expand S first, then T we get just
797 -- For H98, do check the type args
798 mappM_ check_arg_type tys
801 | isUnboxedTupleTyCon tc
802 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
803 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
804 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
805 -- Args are allowed to be unlifted, or
806 -- more unboxed tuples, so can't use check_arg_ty
809 = mappM_ check_arg_type tys
812 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
815 tc_arity = tyConArity tc
817 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
818 ubx_tup_msg = ubxArgTyErr ty
820 ----------------------------------------
821 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
822 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
823 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
824 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
829 %************************************************************************
831 \subsection{Checking a theta or source type}
833 %************************************************************************
836 -- Enumerate the contexts in which a "source type", <S>, can occur
840 -- or (N a) where N is a newtype
843 = ClassSCCtxt Name -- Superclasses of clas
844 -- class <S> => C a where ...
845 | SigmaCtxt -- Theta part of a normal for-all type
846 -- f :: <S> => a -> a
847 | DataTyCtxt Name -- Theta part of a data decl
848 -- data <S> => T a = MkT a
849 | TypeCtxt -- Source type in an ordinary type
851 | InstThetaCtxt -- Context of an instance decl
852 -- instance <S> => C [a] where ...
854 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
855 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
856 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
857 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
858 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
862 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
863 checkValidTheta ctxt theta
864 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
866 -------------------------
867 check_valid_theta ctxt []
869 check_valid_theta ctxt theta
870 = getDOpts `thenM` \ dflags ->
871 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
872 mappM_ (check_pred_ty dflags ctxt) theta
874 (_,dups) = removeDups tcCmpPred theta
876 -------------------------
877 check_pred_ty dflags ctxt pred@(ClassP cls tys)
878 = -- Class predicates are valid in all contexts
879 checkTc (arity == n_tys) arity_err `thenM_`
881 -- Check the form of the argument types
882 mappM_ check_arg_type tys `thenM_`
883 checkTc (check_class_pred_tys dflags ctxt tys)
884 (predTyVarErr pred $$ how_to_allow)
887 class_name = className cls
888 arity = classArity cls
890 arity_err = arityErr "Class" class_name arity n_tys
891 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
893 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
894 -- Implicit parameters only allows in type
895 -- signatures; not in instance decls, superclasses etc
896 -- The reason for not allowing implicit params in instances is a bit subtle
897 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
898 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
899 -- discharge all the potential usas of the ?x in e. For example, a
900 -- constraint Foo [Int] might come out of e,and applying the
901 -- instance decl would show up two uses of ?x.
904 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
906 -------------------------
907 check_class_pred_tys dflags ctxt tys
909 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
910 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
911 -- Further checks on head and theta in
912 -- checkInstTermination
913 other -> gla_exts || all tyvar_head tys
915 gla_exts = dopt Opt_GlasgowExts dflags
916 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
918 -------------------------
919 tyvar_head ty -- Haskell 98 allows predicates of form
920 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
921 | otherwise -- where a is a type variable
922 = case tcSplitAppTy_maybe ty of
923 Just (ty, _) -> tyvar_head ty
930 is ambiguous if P contains generic variables
931 (i.e. one of the Vs) that are not mentioned in tau
933 However, we need to take account of functional dependencies
934 when we speak of 'mentioned in tau'. Example:
935 class C a b | a -> b where ...
937 forall x y. (C x y) => x
938 is not ambiguous because x is mentioned and x determines y
940 NB; the ambiguity check is only used for *user* types, not for types
941 coming from inteface files. The latter can legitimately have
942 ambiguous types. Example
944 class S a where s :: a -> (Int,Int)
945 instance S Char where s _ = (1,1)
946 f:: S a => [a] -> Int -> (Int,Int)
947 f (_::[a]) x = (a*x,b)
948 where (a,b) = s (undefined::a)
950 Here the worker for f gets the type
951 fw :: forall a. S a => Int -> (# Int, Int #)
953 If the list of tv_names is empty, we have a monotype, and then we
954 don't need to check for ambiguity either, because the test can't fail
958 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
959 checkAmbiguity forall_tyvars theta tau_tyvars
960 = mappM_ complain (filter is_ambig theta)
962 complain pred = addErrTc (ambigErr pred)
963 extended_tau_vars = grow theta tau_tyvars
965 -- Only a *class* predicate can give rise to ambiguity
966 -- An *implicit parameter* cannot. For example:
967 -- foo :: (?x :: [a]) => Int
969 -- is fine. The call site will suppply a particular 'x'
970 is_ambig pred = isClassPred pred &&
971 any ambig_var (varSetElems (tyVarsOfPred pred))
973 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
974 not (ct_var `elemVarSet` extended_tau_vars)
977 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
978 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
979 ptext SLIT("must be reachable from the type after the '=>'"))]
982 In addition, GHC insists that at least one type variable
983 in each constraint is in V. So we disallow a type like
984 forall a. Eq b => b -> b
985 even in a scope where b is in scope.
988 checkFreeness forall_tyvars theta
989 = mappM_ complain (filter is_free theta)
991 is_free pred = not (isIPPred pred)
992 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
993 bound_var ct_var = ct_var `elem` forall_tyvars
994 complain pred = addErrTc (freeErr pred)
997 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
998 ptext SLIT("are already in scope"),
999 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1004 checkThetaCtxt ctxt theta
1005 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1006 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1008 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1009 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1010 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1011 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1013 arityErr kind name n m
1014 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1015 n_arguments <> comma, text "but has been given", int m]
1017 n_arguments | n == 0 = ptext SLIT("no arguments")
1018 | n == 1 = ptext SLIT("1 argument")
1019 | True = hsep [int n, ptext SLIT("arguments")]
1023 %************************************************************************
1025 \subsection{Checking for a decent instance head type}
1027 %************************************************************************
1029 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1030 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1032 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1033 flag is on, or (2)~the instance is imported (they must have been
1034 compiled elsewhere). In these cases, we let them go through anyway.
1036 We can also have instances for functions: @instance Foo (a -> b) ...@.
1039 checkValidInstHead :: Type -> TcM (Class, [TcType])
1041 checkValidInstHead ty -- Should be a source type
1042 = case tcSplitPredTy_maybe ty of {
1043 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1046 case getClassPredTys_maybe pred of {
1047 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1050 getDOpts `thenM` \ dflags ->
1051 mappM_ check_arg_type tys `thenM_`
1052 check_inst_head dflags clas tys `thenM_`
1056 check_inst_head dflags clas tys
1057 -- If GlasgowExts then check at least one isn't a type variable
1058 | dopt Opt_GlasgowExts dflags
1059 = mapM_ check_one tys
1061 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1063 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1064 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1067 (first_ty : _) = tys
1069 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1070 text "where T is not a synonym, and a,b,c are distinct type variables")
1072 -- For now, I only allow tau-types (not polytypes) in
1073 -- the head of an instance decl.
1074 -- E.g. instance C (forall a. a->a) is rejected
1075 -- One could imagine generalising that, but I'm not sure
1076 -- what all the consequences might be
1077 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1078 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1080 instTypeErr pp_ty msg
1081 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1086 %************************************************************************
1088 \subsection{Checking instance for termination}
1090 %************************************************************************
1094 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1095 checkValidInstance tyvars theta clas inst_tys
1096 = do { gla_exts <- doptM Opt_GlasgowExts
1097 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1099 ; checkValidTheta InstThetaCtxt theta
1100 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1102 -- Check that instance inference will terminate (if we care)
1103 -- For Haskell 98, checkValidTheta has already done that
1104 ; when (gla_exts && not undecidable_ok) $
1105 checkInstTermination theta inst_tys
1107 -- The Coverage Condition
1108 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1109 (instTypeErr (pprClassPred clas inst_tys) msg)
1112 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1115 Termination test: each assertion in the context satisfies
1116 (1) no variable has more occurrences in the assertion than in the head, and
1117 (2) the assertion has fewer constructors and variables (taken together
1118 and counting repetitions) than the head.
1119 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1120 (which have already been checked) guarantee termination.
1122 The underlying idea is that
1124 for any ground substitution, each assertion in the
1125 context has fewer type constructors than the head.
1129 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1130 checkInstTermination theta tys
1131 = do { mappM_ (check_nomore (fvTypes tys)) theta
1132 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1134 check_nomore :: [TyVar] -> PredType -> TcM ()
1135 check_nomore fvs pred
1136 = checkTc (null (fvPred pred \\ fvs))
1137 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1139 check_smaller :: Int -> PredType -> TcM ()
1140 check_smaller n pred
1141 = checkTc (sizePred pred < n)
1142 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1144 predUndecErr pred msg = sep [msg,
1145 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1147 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1148 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1149 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1151 -- Free variables of a type, retaining repetitions, and expanding synonyms
1152 fvType :: Type -> [TyVar]
1153 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1154 fvType (TyVarTy tv) = [tv]
1155 fvType (TyConApp _ tys) = fvTypes tys
1156 fvType (NoteTy _ ty) = fvType ty
1157 fvType (PredTy pred) = fvPred pred
1158 fvType (FunTy arg res) = fvType arg ++ fvType res
1159 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1160 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1162 fvTypes :: [Type] -> [TyVar]
1163 fvTypes tys = concat (map fvType tys)
1165 fvPred :: PredType -> [TyVar]
1166 fvPred (ClassP _ tys') = fvTypes tys'
1167 fvPred (IParam _ ty) = fvType ty
1168 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1170 -- Size of a type: the number of variables and constructors
1171 sizeType :: Type -> Int
1172 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1173 sizeType (TyVarTy _) = 1
1174 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1175 sizeType (NoteTy _ ty) = sizeType ty
1176 sizeType (PredTy pred) = sizePred pred
1177 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1178 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1179 sizeType (ForAllTy _ ty) = sizeType ty
1181 sizeTypes :: [Type] -> Int
1182 sizeTypes xs = sum (map sizeType xs)
1184 sizePred :: PredType -> Int
1185 sizePred (ClassP _ tys') = sizeTypes tys'
1186 sizePred (IParam _ ty) = sizeType ty
1187 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2