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
83 import Control.Monad ( when )
84 import Data.List ( (\\) )
88 %************************************************************************
90 Instantiation in general
92 %************************************************************************
95 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
96 -> TcType -- Type to instantiate
97 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
98 tcInstType inst_tyvars ty
99 = case tcSplitForAllTys ty of
100 ([], rho) -> let -- There may be overloading despite no type variables;
101 -- (?x :: Int) => Int -> Int
102 (theta, tau) = tcSplitPhiTy rho
104 return ([], theta, tau)
106 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
108 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
109 -- Either the tyvars are freshly made, by inst_tyvars,
110 -- or (in the call from tcSkolSigType) any nested foralls
111 -- have different binders. Either way, zipTopTvSubst is ok
113 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
114 ; return (tyvars', theta, tau) }
118 %************************************************************************
122 %************************************************************************
125 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
127 = do { us <- newUniqueSupply
128 ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
130 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
132 newKindVar :: TcM TcKind
133 newKindVar = do { uniq <- newUnique
134 ; ref <- newMutVar Flexi
135 ; return (mkTyVarTy (mkKindVar uniq ref)) }
137 newKindVars :: Int -> TcM [TcKind]
138 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
142 %************************************************************************
144 SkolemTvs (immutable)
146 %************************************************************************
149 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
150 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
152 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
153 -- Instantiate a type signature with skolem constants, but
154 -- do *not* give them fresh names, because we want the name to
155 -- be in the type environment -- it is lexically scoped.
156 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
158 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
159 -- Make skolem constants, but do *not* give them new names, as above
160 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
163 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
164 -- Instantiate a type with fresh skolem constants
165 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
167 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
168 tcInstSkolTyVar info tyvar
169 = do { uniq <- newUnique
170 ; let name = setNameUnique (tyVarName tyvar) uniq
171 kind = tyVarKind tyvar
172 ; return (mkSkolTyVar name kind info) }
174 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
175 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
179 %************************************************************************
181 MetaTvs (meta type variables; mutable)
183 %************************************************************************
186 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
187 -- Make a new meta tyvar out of thin air
188 newMetaTyVar box_info kind
189 = do { uniq <- newUnique
190 ; ref <- newMutVar Flexi ;
191 ; let name = mkSysTvName uniq fs
192 fs = case box_info of
195 SigTv _ -> FSLIT("a")
196 -- We give BoxTv and TauTv the same string, because
197 -- otherwise we get user-visible differences in error
198 -- messages, which are confusing. If you want to see
199 -- the box_info of each tyvar, use -dppr-debug
200 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
202 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
203 -- Make a new meta tyvar whose Name and Kind
204 -- come from an existing TyVar
205 instMetaTyVar box_info tyvar
206 = do { uniq <- newUnique
207 ; ref <- newMutVar Flexi ;
208 ; let name = setNameUnique (tyVarName tyvar) uniq
209 kind = tyVarKind tyvar
210 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
212 readMetaTyVar :: TyVar -> TcM MetaDetails
213 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
214 readMutVar (metaTvRef tyvar)
216 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
218 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
220 writeMetaTyVar tyvar ty
221 | not (isMetaTyVar tyvar)
222 = pprTrace "writeMetaTyVar" (ppr tyvar) $
226 = ASSERT( isMetaTyVar tyvar )
227 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
228 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
229 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
237 %************************************************************************
241 %************************************************************************
244 newFlexiTyVar :: Kind -> TcM TcTyVar
245 newFlexiTyVar kind = newMetaTyVar TauTv kind
247 newFlexiTyVarTy :: Kind -> TcM TcType
249 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
250 returnM (TyVarTy tc_tyvar)
252 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
253 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
255 tcInstTyVar :: TyVar -> TcM TcTyVar
256 -- Instantiate with a META type variable
257 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
259 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
260 -- Instantiate with META type variables
262 = do { tc_tvs <- mapM tcInstTyVar tyvars
263 ; let tys = mkTyVarTys tc_tvs
264 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
265 -- Since the tyvars are freshly made,
266 -- they cannot possibly be captured by
267 -- any existing for-alls. Hence zipTopTvSubst
271 %************************************************************************
275 %************************************************************************
278 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
279 -- Instantiate with meta SigTvs
280 tcInstSigTyVars skol_info tyvars
281 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
283 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
285 | isSkolemTyVar sig_tv
286 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
288 = ASSERT( isSigTyVar sig_tv )
289 do { ty <- zonkTcTyVar sig_tv
290 ; return (tcGetTyVar "zonkSigTyVar" ty) }
291 -- 'ty' is bound to be a type variable, because SigTvs
292 -- can only be unified with type variables
296 %************************************************************************
300 %************************************************************************
303 newBoxyTyVar :: Kind -> TcM BoxyTyVar
304 newBoxyTyVar kind = newMetaTyVar BoxTv kind
306 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
307 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
309 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
310 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
312 readFilledBox :: BoxyTyVar -> TcM TcType
313 -- Read the contents of the box, which should be filled in by now
314 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
315 do { cts <- readMetaTyVar box_tv
317 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
318 Indirect ty -> return ty }
320 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
321 -- Instantiate with a BOXY type variable
322 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
326 %************************************************************************
328 \subsection{Putting and getting mutable type variables}
330 %************************************************************************
332 But it's more fun to short out indirections on the way: If this
333 version returns a TyVar, then that TyVar is unbound. If it returns
334 any other type, then there might be bound TyVars embedded inside it.
336 We return Nothing iff the original box was unbound.
339 data LookupTyVarResult -- The result of a lookupTcTyVar call
340 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
343 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
345 = ASSERT( isTcTyVar tyvar )
347 SkolemTv _ -> return (DoneTv details)
348 MetaTv _ ref -> do { meta_details <- readMutVar ref
349 ; case meta_details of
350 Indirect ty -> return (IndirectTv ty)
351 Flexi -> return (DoneTv details) }
353 details = tcTyVarDetails tyvar
356 -- gaw 2004 We aren't shorting anything out anymore, at least for now
358 | not (isTcTyVar tyvar)
359 = pprTrace "getTcTyVar" (ppr tyvar) $
360 returnM (Just (mkTyVarTy tyvar))
363 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
364 readMetaTyVar tyvar `thenM` \ maybe_ty ->
366 Just ty -> short_out ty `thenM` \ ty' ->
367 writeMetaTyVar tyvar (Just ty') `thenM_`
370 Nothing -> returnM Nothing
372 short_out :: TcType -> TcM TcType
373 short_out ty@(TyVarTy tyvar)
374 | not (isTcTyVar tyvar)
378 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
380 Just ty' -> short_out ty' `thenM` \ ty' ->
381 writeMetaTyVar tyvar (Just ty') `thenM_`
386 short_out other_ty = returnM other_ty
391 %************************************************************************
393 \subsection{Zonking -- the exernal interfaces}
395 %************************************************************************
397 ----------------- Type variables
400 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
401 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
403 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
404 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
405 returnM (tyVarsOfTypes tys)
407 zonkTcTyVar :: TcTyVar -> TcM TcType
408 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
409 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
412 ----------------- Types
415 zonkTcType :: TcType -> TcM TcType
416 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
418 zonkTcTypes :: [TcType] -> TcM [TcType]
419 zonkTcTypes tys = mappM zonkTcType tys
421 zonkTcClassConstraints cts = mappM zonk cts
422 where zonk (clas, tys)
423 = zonkTcTypes tys `thenM` \ new_tys ->
424 returnM (clas, new_tys)
426 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
427 zonkTcThetaType theta = mappM zonkTcPredType theta
429 zonkTcPredType :: TcPredType -> TcM TcPredType
430 zonkTcPredType (ClassP c ts)
431 = zonkTcTypes ts `thenM` \ new_ts ->
432 returnM (ClassP c new_ts)
433 zonkTcPredType (IParam n t)
434 = zonkTcType t `thenM` \ new_t ->
435 returnM (IParam n new_t)
436 zonkTcPredType (EqPred t1 t2)
437 = zonkTcType t1 `thenM` \ new_t1 ->
438 zonkTcType t2 `thenM` \ new_t2 ->
439 returnM (EqPred new_t1 new_t2)
442 ------------------- These ...ToType, ...ToKind versions
443 are used at the end of type checking
446 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
447 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
448 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
449 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
450 -- The meta tyvar is updated to point to the new regular TyVar. Now any
451 -- bound occurences of the original type variable will get zonked to
452 -- the immutable version.
454 -- We leave skolem TyVars alone; they are immutable.
455 zonkQuantifiedTyVar tv
456 | isSkolemTyVar tv = return tv
457 -- It might be a skolem type variable,
458 -- for example from a user type signature
460 | otherwise -- It's a meta-type-variable
461 = do { details <- readMetaTyVar tv
463 -- Create the new, frozen, regular type variable
464 ; let final_kind = defaultKind (tyVarKind tv)
465 final_tv = mkTyVar (tyVarName tv) final_kind
467 -- Bind the meta tyvar to the new tyvar
469 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
471 -- [Sept 04] I don't think this should happen
472 -- See note [Silly Type Synonym]
474 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
476 -- Return the new tyvar
480 [Silly Type Synonyms]
483 type C u a = u -- Note 'a' unused
485 foo :: (forall a. C u a -> C u a) -> u
489 bar = foo (\t -> t + t)
491 * From the (\t -> t+t) we get type {Num d} => d -> d
494 * Now unify with type of foo's arg, and we get:
495 {Num (C d a)} => C d a -> C d a
498 * Now abstract over the 'a', but float out the Num (C d a) constraint
499 because it does not 'really' mention a. (see exactTyVarsOfType)
500 The arg to foo becomes
503 * So we get a dict binding for Num (C d a), which is zonked to give
505 [Note Sept 04: now that we are zonking quantified type variables
506 on construction, the 'a' will be frozen as a regular tyvar on
507 quantification, so the floated dict will still have type (C d a).
508 Which renders this whole note moot; happily!]
510 * Then the /\a abstraction has a zonked 'a' in it.
512 All very silly. I think its harmless to ignore the problem. We'll end up with
513 a /\a in the final result but all the occurrences of a will be zonked to ()
516 %************************************************************************
518 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
520 %* For internal use only! *
522 %************************************************************************
525 -- For unbound, mutable tyvars, zonkType uses the function given to it
526 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
527 -- type variable and zonks the kind too
529 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
530 -- see zonkTcType, and zonkTcTypeToType
533 zonkType unbound_var_fn ty
536 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
538 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
539 returnM (TyConApp tc tys')
541 go (PredTy p) = go_pred p `thenM` \ p' ->
544 go (FunTy arg res) = go arg `thenM` \ arg' ->
545 go res `thenM` \ res' ->
546 returnM (FunTy arg' res')
548 go (AppTy fun arg) = go fun `thenM` \ fun' ->
549 go arg `thenM` \ arg' ->
550 returnM (mkAppTy fun' arg')
551 -- NB the mkAppTy; we might have instantiated a
552 -- type variable to a type constructor, so we need
553 -- to pull the TyConApp to the top.
555 -- The two interesting cases!
556 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
557 | otherwise = return (TyVarTy tyvar)
558 -- Ordinary (non Tc) tyvars occur inside quantified types
560 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
561 go ty `thenM` \ ty' ->
562 returnM (ForAllTy tyvar ty')
564 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
565 returnM (ClassP c tys')
566 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
567 returnM (IParam n ty')
568 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
569 go ty2 `thenM` \ ty2' ->
570 returnM (EqPred ty1' ty2')
572 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
573 -> TcTyVar -> TcM TcType
574 zonk_tc_tyvar unbound_var_fn tyvar
575 | not (isMetaTyVar tyvar) -- Skolems
576 = returnM (TyVarTy tyvar)
578 | otherwise -- Mutables
579 = do { cts <- readMetaTyVar tyvar
581 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
582 Indirect ty -> zonkType unbound_var_fn ty }
587 %************************************************************************
591 %************************************************************************
594 readKindVar :: KindVar -> TcM (MetaDetails)
595 writeKindVar :: KindVar -> TcKind -> TcM ()
596 readKindVar kv = readMutVar (kindVarRef kv)
597 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
600 zonkTcKind :: TcKind -> TcM TcKind
601 zonkTcKind k = zonkTcType k
604 zonkTcKindToKind :: TcKind -> TcM Kind
605 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
606 -- Haskell specifies that * is to be used, so we follow that.
607 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
610 %************************************************************************
612 \subsection{Checking a user type}
614 %************************************************************************
616 When dealing with a user-written type, we first translate it from an HsType
617 to a Type, performing kind checking, and then check various things that should
618 be true about it. We don't want to perform these checks at the same time
619 as the initial translation because (a) they are unnecessary for interface-file
620 types and (b) when checking a mutually recursive group of type and class decls,
621 we can't "look" at the tycons/classes yet. Also, the checks are are rather
622 diverse, and used to really mess up the other code.
624 One thing we check for is 'rank'.
626 Rank 0: monotypes (no foralls)
627 Rank 1: foralls at the front only, Rank 0 inside
628 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
630 basic ::= tyvar | T basic ... basic
632 r2 ::= forall tvs. cxt => r2a
633 r2a ::= r1 -> r2a | basic
634 r1 ::= forall tvs. cxt => r0
635 r0 ::= r0 -> r0 | basic
637 Another thing is to check that type synonyms are saturated.
638 This might not necessarily show up in kind checking.
640 data T k = MkT (k Int)
645 checkValidType :: UserTypeCtxt -> Type -> TcM ()
646 -- Checks that the type is valid for the given context
647 checkValidType ctxt ty
648 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
649 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
651 rank | gla_exts = Arbitrary
653 = case ctxt of -- Haskell 98
655 LamPatSigCtxt -> Rank 0
656 BindPatSigCtxt -> Rank 0
657 DefaultDeclCtxt-> Rank 0
659 TySynCtxt _ -> Rank 0
660 ExprSigCtxt -> Rank 1
661 FunSigCtxt _ -> Rank 1
662 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
663 -- constructor, hence rank 1
664 ForSigCtxt _ -> Rank 1
665 RuleSigCtxt _ -> Rank 1
666 SpecInstCtxt -> Rank 1
668 actual_kind = typeKind ty
670 kind_ok = case ctxt of
671 TySynCtxt _ -> True -- Any kind will do
672 ResSigCtxt -> isSubOpenTypeKind actual_kind
673 ExprSigCtxt -> isSubOpenTypeKind actual_kind
674 GenPatCtxt -> isLiftedTypeKind actual_kind
675 ForSigCtxt _ -> isLiftedTypeKind actual_kind
676 other -> isSubArgTypeKind actual_kind
678 ubx_tup | not gla_exts = UT_NotOk
679 | otherwise = case ctxt of
683 -- Unboxed tuples ok in function results,
684 -- but for type synonyms we allow them even at
687 -- Check that the thing has kind Type, and is lifted if necessary
688 checkTc kind_ok (kindErr actual_kind) `thenM_`
690 -- Check the internal validity of the type itself
691 check_poly_type rank ubx_tup ty `thenM_`
693 traceTc (text "checkValidType done" <+> ppr ty)
698 data Rank = Rank Int | Arbitrary
700 decRank :: Rank -> Rank
701 decRank Arbitrary = Arbitrary
702 decRank (Rank n) = Rank (n-1)
704 ----------------------------------------
705 data UbxTupFlag = UT_Ok | UT_NotOk
706 -- The "Ok" version means "ok if -fglasgow-exts is on"
708 ----------------------------------------
709 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
710 check_poly_type (Rank 0) ubx_tup ty
711 = check_tau_type (Rank 0) ubx_tup ty
713 check_poly_type rank ubx_tup ty
714 | null tvs && null theta
715 = check_tau_type rank ubx_tup ty
717 = do { check_valid_theta SigmaCtxt theta
718 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
719 ; checkFreeness tvs theta
720 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
722 (tvs, theta, tau) = tcSplitSigmaTy ty
724 ----------------------------------------
725 check_arg_type :: Type -> TcM ()
726 -- The sort of type that can instantiate a type variable,
727 -- or be the argument of a type constructor.
728 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
729 -- Other unboxed types are very occasionally allowed as type
730 -- arguments depending on the kind of the type constructor
732 -- For example, we want to reject things like:
734 -- instance Ord a => Ord (forall s. T s a)
736 -- g :: T s (forall b.b)
738 -- NB: unboxed tuples can have polymorphic or unboxed args.
739 -- This happens in the workers for functions returning
740 -- product types with polymorphic components.
741 -- But not in user code.
742 -- Anyway, they are dealt with by a special case in check_tau_type
745 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
746 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
748 ----------------------------------------
749 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
750 -- Rank is allowed rank for function args
751 -- No foralls otherwise
753 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
754 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
755 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
757 -- Naked PredTys don't usually show up, but they can as a result of
758 -- {-# SPECIALISE instance Ord Char #-}
759 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
760 -- are handled, but the quick thing is just to permit PredTys here.
761 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
762 check_pred_ty dflags TypeCtxt sty
764 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
765 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
766 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
767 check_poly_type rank UT_Ok res_ty
769 check_tau_type rank ubx_tup (AppTy ty1 ty2)
770 = check_arg_type ty1 `thenM_` check_arg_type ty2
772 check_tau_type rank ubx_tup (NoteTy other_note ty)
773 = check_tau_type rank ubx_tup ty
775 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
777 = do { -- It's OK to have an *over-applied* type synonym
778 -- data Tree a b = ...
779 -- type Foo a = Tree [a]
780 -- f :: Foo a b -> ...
782 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
783 Nothing -> failWithTc arity_msg
785 ; gla_exts <- doptM Opt_GlasgowExts
787 -- If -fglasgow-exts then don't check the type arguments
788 -- This allows us to instantiate a synonym defn with a
789 -- for-all type, or with a partially-applied type synonym.
790 -- e.g. type T a b = a
793 -- Here, T is partially applied, so it's illegal in H98.
794 -- But if you expand S first, then T we get just
799 -- For H98, do check the type args
800 mappM_ check_arg_type tys
803 | isUnboxedTupleTyCon tc
804 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
805 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
806 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
807 -- Args are allowed to be unlifted, or
808 -- more unboxed tuples, so can't use check_arg_ty
811 = mappM_ check_arg_type tys
814 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
817 tc_arity = tyConArity tc
819 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
820 ubx_tup_msg = ubxArgTyErr ty
822 ----------------------------------------
823 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
824 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
825 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
826 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
831 %************************************************************************
833 \subsection{Checking a theta or source type}
835 %************************************************************************
838 -- Enumerate the contexts in which a "source type", <S>, can occur
842 -- or (N a) where N is a newtype
845 = ClassSCCtxt Name -- Superclasses of clas
846 -- class <S> => C a where ...
847 | SigmaCtxt -- Theta part of a normal for-all type
848 -- f :: <S> => a -> a
849 | DataTyCtxt Name -- Theta part of a data decl
850 -- data <S> => T a = MkT a
851 | TypeCtxt -- Source type in an ordinary type
853 | InstThetaCtxt -- Context of an instance decl
854 -- instance <S> => C [a] where ...
856 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
857 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
858 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
859 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
860 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
864 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
865 checkValidTheta ctxt theta
866 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
868 -------------------------
869 check_valid_theta ctxt []
871 check_valid_theta ctxt theta
872 = getDOpts `thenM` \ dflags ->
873 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
874 mappM_ (check_pred_ty dflags ctxt) theta
876 (_,dups) = removeDups tcCmpPred theta
878 -------------------------
879 check_pred_ty dflags ctxt pred@(ClassP cls tys)
880 = -- Class predicates are valid in all contexts
881 checkTc (arity == n_tys) arity_err `thenM_`
883 -- Check the form of the argument types
884 mappM_ check_arg_type tys `thenM_`
885 checkTc (check_class_pred_tys dflags ctxt tys)
886 (predTyVarErr pred $$ how_to_allow)
889 class_name = className cls
890 arity = classArity cls
892 arity_err = arityErr "Class" class_name arity n_tys
893 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
895 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
896 -- Implicit parameters only allows in type
897 -- signatures; not in instance decls, superclasses etc
898 -- The reason for not allowing implicit params in instances is a bit subtle
899 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
900 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
901 -- discharge all the potential usas of the ?x in e. For example, a
902 -- constraint Foo [Int] might come out of e,and applying the
903 -- instance decl would show up two uses of ?x.
906 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
908 -------------------------
909 check_class_pred_tys dflags ctxt tys
911 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
912 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
913 -- Further checks on head and theta in
914 -- checkInstTermination
915 other -> gla_exts || all tyvar_head tys
917 gla_exts = dopt Opt_GlasgowExts dflags
918 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
920 -------------------------
921 tyvar_head ty -- Haskell 98 allows predicates of form
922 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
923 | otherwise -- where a is a type variable
924 = case tcSplitAppTy_maybe ty of
925 Just (ty, _) -> tyvar_head ty
932 is ambiguous if P contains generic variables
933 (i.e. one of the Vs) that are not mentioned in tau
935 However, we need to take account of functional dependencies
936 when we speak of 'mentioned in tau'. Example:
937 class C a b | a -> b where ...
939 forall x y. (C x y) => x
940 is not ambiguous because x is mentioned and x determines y
942 NB; the ambiguity check is only used for *user* types, not for types
943 coming from inteface files. The latter can legitimately have
944 ambiguous types. Example
946 class S a where s :: a -> (Int,Int)
947 instance S Char where s _ = (1,1)
948 f:: S a => [a] -> Int -> (Int,Int)
949 f (_::[a]) x = (a*x,b)
950 where (a,b) = s (undefined::a)
952 Here the worker for f gets the type
953 fw :: forall a. S a => Int -> (# Int, Int #)
955 If the list of tv_names is empty, we have a monotype, and then we
956 don't need to check for ambiguity either, because the test can't fail
960 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
961 checkAmbiguity forall_tyvars theta tau_tyvars
962 = mappM_ complain (filter is_ambig theta)
964 complain pred = addErrTc (ambigErr pred)
965 extended_tau_vars = grow theta tau_tyvars
967 -- Only a *class* predicate can give rise to ambiguity
968 -- An *implicit parameter* cannot. For example:
969 -- foo :: (?x :: [a]) => Int
971 -- is fine. The call site will suppply a particular 'x'
972 is_ambig pred = isClassPred pred &&
973 any ambig_var (varSetElems (tyVarsOfPred pred))
975 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
976 not (ct_var `elemVarSet` extended_tau_vars)
979 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
980 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
981 ptext SLIT("must be reachable from the type after the '=>'"))]
984 In addition, GHC insists that at least one type variable
985 in each constraint is in V. So we disallow a type like
986 forall a. Eq b => b -> b
987 even in a scope where b is in scope.
990 checkFreeness forall_tyvars theta
991 = mappM_ complain (filter is_free theta)
993 is_free pred = not (isIPPred pred)
994 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
995 bound_var ct_var = ct_var `elem` forall_tyvars
996 complain pred = addErrTc (freeErr pred)
999 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1000 ptext SLIT("are already in scope"),
1001 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1006 checkThetaCtxt ctxt theta
1007 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1008 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1010 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1011 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1012 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1013 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1015 arityErr kind name n m
1016 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1017 n_arguments <> comma, text "but has been given", int m]
1019 n_arguments | n == 0 = ptext SLIT("no arguments")
1020 | n == 1 = ptext SLIT("1 argument")
1021 | True = hsep [int n, ptext SLIT("arguments")]
1025 %************************************************************************
1027 \subsection{Checking for a decent instance head type}
1029 %************************************************************************
1031 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1032 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1034 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1035 flag is on, or (2)~the instance is imported (they must have been
1036 compiled elsewhere). In these cases, we let them go through anyway.
1038 We can also have instances for functions: @instance Foo (a -> b) ...@.
1041 checkValidInstHead :: Type -> TcM (Class, [TcType])
1043 checkValidInstHead ty -- Should be a source type
1044 = case tcSplitPredTy_maybe ty of {
1045 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1048 case getClassPredTys_maybe pred of {
1049 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1052 getDOpts `thenM` \ dflags ->
1053 mappM_ check_arg_type tys `thenM_`
1054 check_inst_head dflags clas tys `thenM_`
1058 check_inst_head dflags clas tys
1059 -- If GlasgowExts then check at least one isn't a type variable
1060 | dopt Opt_GlasgowExts dflags
1061 = mapM_ check_one tys
1063 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1065 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1066 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1069 (first_ty : _) = tys
1071 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1072 text "where T is not a synonym, and a,b,c are distinct type variables")
1074 -- For now, I only allow tau-types (not polytypes) in
1075 -- the head of an instance decl.
1076 -- E.g. instance C (forall a. a->a) is rejected
1077 -- One could imagine generalising that, but I'm not sure
1078 -- what all the consequences might be
1079 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1080 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1082 instTypeErr pp_ty msg
1083 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1088 %************************************************************************
1090 \subsection{Checking instance for termination}
1092 %************************************************************************
1096 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1097 checkValidInstance tyvars theta clas inst_tys
1098 = do { gla_exts <- doptM Opt_GlasgowExts
1099 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1101 ; checkValidTheta InstThetaCtxt theta
1102 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1104 -- Check that instance inference will terminate (if we care)
1105 -- For Haskell 98, checkValidTheta has already done that
1106 ; when (gla_exts && not undecidable_ok) $
1107 mapM_ failWithTc (checkInstTermination inst_tys theta)
1109 -- The Coverage Condition
1110 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1111 (instTypeErr (pprClassPred clas inst_tys) msg)
1114 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1117 Termination test: each assertion in the context satisfies
1118 (1) no variable has more occurrences in the assertion than in the head, and
1119 (2) the assertion has fewer constructors and variables (taken together
1120 and counting repetitions) than the head.
1121 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1122 (which have already been checked) guarantee termination.
1124 The underlying idea is that
1126 for any ground substitution, each assertion in the
1127 context has fewer type constructors than the head.
1131 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1132 checkInstTermination tys theta
1133 = mapCatMaybes check theta
1136 size = sizeTypes tys
1138 | not (null (fvPred pred \\ fvs))
1139 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1140 | sizePred pred >= size
1141 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1145 predUndecErr pred msg = sep [msg,
1146 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1148 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1149 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1150 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1152 -- Free variables of a type, retaining repetitions, and expanding synonyms
1153 fvType :: Type -> [TyVar]
1154 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1155 fvType (TyVarTy tv) = [tv]
1156 fvType (TyConApp _ tys) = fvTypes tys
1157 fvType (NoteTy _ ty) = fvType ty
1158 fvType (PredTy pred) = fvPred pred
1159 fvType (FunTy arg res) = fvType arg ++ fvType res
1160 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1161 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1163 fvTypes :: [Type] -> [TyVar]
1164 fvTypes tys = concat (map fvType tys)
1166 fvPred :: PredType -> [TyVar]
1167 fvPred (ClassP _ tys') = fvTypes tys'
1168 fvPred (IParam _ ty) = fvType ty
1169 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1171 -- Size of a type: the number of variables and constructors
1172 sizeType :: Type -> Int
1173 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1174 sizeType (TyVarTy _) = 1
1175 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1176 sizeType (NoteTy _ ty) = sizeType ty
1177 sizeType (PredTy pred) = sizePred pred
1178 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1179 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1180 sizeType (ForAllTy _ ty) = sizeType ty
1182 sizeTypes :: [Type] -> Int
1183 sizeTypes xs = sum (map sizeType xs)
1185 sizePred :: PredType -> Int
1186 sizePred (ClassP _ tys') = sizeTypes tys'
1187 sizePred (IParam _ ty) = sizeType ty
1188 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2