2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubPat, tcSubExp, tcSub, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTheta,
14 unifyKind, unifyKinds, unifyFunKind,
17 --------------------------------
19 Expected(..), tcInfer, readExpectedType,
20 zapExpectedType, zapExpectedTo, zapExpectedBranches,
21 subFunTys, unifyFunTys,
22 zapToListTy, unifyListTy,
23 zapToTyConApp, unifyTyConApp,
27 #include "HsVersions.h"
29 import HsSyn ( HsExpr(..) , MatchGroup(..), HsMatchContext(..),
30 hsLMatchPats, pprMatches, pprMatchContext )
31 import TcHsSyn ( mkHsDictLet, mkHsDictLam,
32 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
33 import TypeRep ( Type(..), PredType(..) )
35 import TcRnMonad -- TcType, amongst others
36 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
37 TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
38 SkolemInfo( GenSkol ), MetaDetails(..),
39 pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp,
40 tcSplitAppTy_maybe, tcEqType,
41 tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar,
42 typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
43 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
44 pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView )
45 import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
46 openTypeKind, liftedTypeKind, mkArrowKind,
47 isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
48 isSubKind, pprKind, splitKindFunTys )
49 import Inst ( newDicts, instToId, tcInstCall )
50 import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
51 tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
52 newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
53 readKindVar, writeKindVar )
54 import TcSimplify ( tcSimplifyCheck )
55 import TcIface ( checkWiredInTyCon )
56 import TcEnv ( tcGetGlobalTyVars, findGlobals )
57 import TyCon ( TyCon, tyConArity, tyConTyVars, isFunTyCon, isSynTyCon,
59 import TysWiredIn ( listTyCon )
60 import Id ( Id, mkSysLocal )
61 import Var ( Var, varName, tyVarKind )
62 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
64 import Name ( Name, isSystemName, mkSysTvName )
65 import ErrUtils ( Message )
66 import SrcLoc ( noLoc )
67 import BasicTypes ( Arity )
68 import Util ( notNull, equalLength )
74 * A hole is always filled in with an ordinary type, not another hole.
76 %************************************************************************
78 \subsection{'hole' type variables}
80 %************************************************************************
83 newHole = newMutVar (error "Empty hole in typechecker")
85 tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
87 = do { hole <- newHole
88 ; res <- tc_infer (Infer hole)
89 ; res_ty <- readMutVar hole
90 ; return (res, res_ty) }
92 readExpectedType :: Expected ty -> TcM ty
93 readExpectedType (Infer hole) = readMutVar hole
94 readExpectedType (Check ty) = returnM ty
96 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
97 -- In the inference case, ensure we have a monotype
98 -- (including an unboxed tuple)
99 zapExpectedType (Infer hole) kind
100 = do { ty <- newTyFlexiVarTy kind ;
101 writeMutVar hole ty ;
104 zapExpectedType (Check ty) kind
105 | typeKind ty `isSubKind` kind = return ty
106 | otherwise = do { ty1 <- newTyFlexiVarTy kind
109 -- The unify is to ensure that 'ty' has the desired kind
110 -- For example, in (case e of r -> b) we push an OpenTypeKind
113 zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
114 -- If there is more than one branch in a case expression,
115 -- and exp_ty is a 'hole', all branches must be types, not type schemes,
116 -- otherwise the order in which we check them would affect the result.
117 zapExpectedBranches (MatchGroup [match] _) exp_ty
118 = return exp_ty -- One branch
119 zapExpectedBranches matches (Check ty)
121 zapExpectedBranches matches (Infer hole)
122 = do { -- Many branches, and inference mode,
123 -- so switch to checking mode with a monotype
124 ty <- newTyFlexiVarTy openTypeKind
125 ; writeMutVar hole ty
126 ; return (Check ty) }
128 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
129 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
130 zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
131 -- See Note [Zonk return type]
133 instance Outputable ty => Outputable (Expected ty) where
134 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
135 ppr (Infer hole) = ptext SLIT("Inferring type")
139 %************************************************************************
141 \subsection[Unify-fun]{@unifyFunTy@}
143 %************************************************************************
145 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
146 creation of type variables.
148 * subFunTy is used when we might be faced with a "hole" type variable,
149 in which case we should create two new holes.
151 * unifyFunTy is used when we expect to encounter only "ordinary"
152 type variables, so we should create new ordinary type variables
155 subFunTys :: HsMatchContext Name
157 -> Expected TcRhoType -- Fail if ty isn't a function type
158 -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
161 subFunTys ctxt (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
162 = -- This is the interesting case
163 ASSERT( null null_matches )
164 do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
165 ; res_hole <- newHole
168 ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
170 -- Extract the answers
171 ; arg_tys <- mapM readMutVar pat_holes
172 ; res_ty <- readMutVar res_hole
174 -- Write the answer into the incoming hole
175 ; writeMutVar hole (mkFunTys arg_tys res_ty)
177 -- And return the answer
180 subFunTys ctxt group@(MatchGroup (match:matches) _) (Check ty) thing_inside
181 = ASSERT( all ((== n_pats) . length . hsLMatchPats) matches )
182 -- Assertion just checks that all the matches have the same number of pats
183 do { (pat_tys, res_ty) <- unifyFunTys msg n_pats ty
184 ; thing_inside (map Check pat_tys) (Check res_ty) }
186 n_pats = length (hsLMatchPats match)
188 FunRhs fun -> ptext SLIT("The equation(s) for") <+> quotes (ppr fun)
189 <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument"))
190 LambdaExpr -> sep [ ptext SLIT("The lambda expression")
191 <+> quotes (pprSetDepth 1 $ pprMatches ctxt group),
192 -- The pprSetDepth makes the abstraction print briefly
193 ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("arguments"))]
194 other -> pprPanic "subFunTys" (pprMatchContext ctxt)
197 unifyFunTys :: SDoc -> Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
198 -- Fail if ty isn't a function type, otherwise return arg and result types
199 -- The result types are guaranteed wobbly if the argument is wobbly
201 -- Does not allocate unnecessary meta variables: if the input already is
202 -- a function, we just take it apart. Not only is this efficient, it's important
203 -- for (a) higher rank: the argument might be of form
204 -- (forall a. ty) -> other
205 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
206 -- blow up with the meta var meets the forall
208 -- (b) GADTs: if the argument is not wobbly we do not want the result to be
211 Error messages from unifyFunTys
212 The first line is passed in as error_herald
214 The abstraction `\Just 1 -> ...' has two arguments
215 but its type `Maybe a -> a' has only one
217 The equation(s) for `f' have two arguments
218 but its type `Maybe a -> a' has only one
220 The section `(f 3)' requires 'f' to take two arguments
221 but its type `Int -> Int' has only one
223 The function 'f' is applied to two arguments
224 but its type `Int -> Int' has only one
227 unifyFunTys error_herald arity ty
228 -- error_herald is the whole first line of the error message above
229 = do { (ok, args, res) <- unify_fun_ty True arity ty
230 ; if ok then return (args, res)
231 else failWithTc (mk_msg (length args)) }
234 = error_herald <> comma $$
235 sep [ptext SLIT("but its type") <+> quotes (pprType ty),
236 if n_actual == 0 then ptext SLIT("has none")
237 else ptext SLIT("has only") <+> speakN n_actual]
239 unify_fun_ty :: Bool -> Arity -> TcRhoType
240 -> TcM (Bool, -- Arity satisfied?
241 [TcSigmaType], -- Arg types found; length <= arity
242 TcRhoType) -- Result type
244 unify_fun_ty use_refinement arity ty
246 = do { res_ty <- wobblify use_refinement ty
247 ; return (True, [], ty) }
249 unify_fun_ty use_refinement arity ty
250 | Just ty' <- tcView ty
251 = unify_fun_ty use_refinement arity ty'
253 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
254 = do { details <- condLookupTcTyVar use_refinement tv
256 IndirectTv use' ty' -> unify_fun_ty use' arity ty'
257 DoneTv (MetaTv ref) -> ASSERT( liftedTypeKind `isSubKind` tyVarKind tv )
258 -- The argument to unifyFunTys is always a type
259 -- Occurs check can't happen, of course
260 do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
261 ; res <- newTyFlexiVarTy openTypeKind
262 ; writeMutVar ref (Indirect (mkFunTys args res))
263 ; return (True, args, res) }
264 DoneTv skol -> return (False, [], ty)
267 unify_fun_ty use_refinement arity ty
268 | Just (arg,res) <- tcSplitFunTy_maybe ty
269 = do { arg' <- wobblify use_refinement arg
270 ; (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
271 ; return (ok, arg':args', res') }
273 unify_fun_ty use_refinement arity ty
274 -- Common cases are all done by now
275 -- At this point we usually have an error, but ty could
276 -- be (a Int Bool), or (a Bool), which can match
277 -- So just use the unifier. But catch any error so we just
278 -- return the success/fail boolean
279 = do { arg <- newTyFlexiVarTy argTypeKind
280 ; res <- newTyFlexiVarTy openTypeKind
281 ; let fun_ty = mkFunTy arg res
282 ; (_, mb_unit) <- tryTc (uTys True ty ty True fun_ty fun_ty)
284 Nothing -> return (False, [], ty) ;
286 do { (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
287 ; return (ok, arg:args', res')
292 ----------------------
293 zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
294 -> Expected TcSigmaType -- Expected type (T a b c)
295 -> TcM [TcType] -- Element types, a b c
296 -- Insists that the Expected type is not a forall-type
297 -- It's used for wired-in tycons, so we call checkWiredInTyCOn
298 -- Precondition: never called with FunTyCon
299 zapToTyConApp tc (Check ty)
300 = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon
301 do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type
303 zapToTyConApp tc (Infer hole)
304 = do { (_, elt_tys, _) <- tcInstTyVars (tyConTyVars tc)
305 ; let tc_app = mkTyConApp tc elt_tys
306 ; writeMutVar hole tc_app
307 ; traceTc (text "zap" <+> ppr tc)
308 ; checkWiredInTyCon tc
311 zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists
312 zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
315 ----------------------
316 unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
318 = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon
319 unify_tc_app (tyConArity tc) True tc ty
320 -- Add a boolean flag to remember whether
321 -- to use the type refinement or not
323 unifyListTy :: TcType -> TcM TcType -- Special case for lists
324 unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
328 unify_tc_app n_args use_refinement tc ty
329 | Just ty' <- tcView ty
330 = unify_tc_app n_args use_refinement tc ty'
332 unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys)
334 = ASSERT( n_args == length arg_tys ) -- ty::*
335 mapM (wobblify use_refinement) arg_tys
337 unify_tc_app n_args use_refinement tc (AppTy fun_ty arg_ty)
338 = do { arg_ty' <- wobblify use_refinement arg_ty
339 ; arg_tys <- unify_tc_app (n_args - 1) use_refinement tc fun_ty
340 ; return (arg_tys ++ [arg_ty']) }
342 unify_tc_app n_args use_refinement tc ty@(TyVarTy tyvar)
343 = do { traceTc (text "unify_tc_app: tyvar" <+> pprTcTyVar tyvar)
344 ; details <- condLookupTcTyVar use_refinement tyvar
346 IndirectTv use' ty' -> unify_tc_app n_args use' tc ty'
347 other -> unify_tc_app_help n_args tc ty
350 unify_tc_app n_args use_refinement tc ty = unify_tc_app_help n_args tc ty
352 unify_tc_app_help n_args tc ty -- Revert to ordinary unification
353 = do { (_, elt_tys, _) <- tcInstTyVars (take n_args (tyConTyVars tc))
354 ; let tc_app = mkTyConApp tc elt_tys
355 ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
356 unifyMisMatch ty tc_app
358 { unifyTauTy ty tc_app
359 ; returnM elt_tys } }
362 ----------------------
363 unifyAppTy :: TcType -- Type to split: m a
364 -> TcM (TcType, TcType) -- (m,a)
367 unifyAppTy ty = unify_app_ty True ty
370 | Just ty' <- tcView ty = unify_app_ty use ty'
372 unify_app_ty use ty@(TyVarTy tyvar)
373 = do { details <- condLookupTcTyVar use tyvar
375 IndirectTv use' ty' -> unify_app_ty use' ty'
376 other -> unify_app_ty_help ty
380 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
381 = do { fun' <- wobblify use fun_ty
382 ; arg' <- wobblify use arg_ty
383 ; return (fun', arg') }
385 | otherwise = unify_app_ty_help ty
387 unify_app_ty_help ty -- Revert to ordinary unification
388 = do { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind)
389 ; arg_ty <- newTyFlexiVarTy liftedTypeKind
390 ; unifyTauTy (mkAppTy fun_ty arg_ty) ty
391 ; return (fun_ty, arg_ty) }
394 ----------------------
395 wobblify :: Bool -- True <=> don't wobblify
398 -- Return a wobbly type. At the moment we do that by
399 -- allocating a fresh meta type variable.
400 wobblify True ty = return ty -- Don't wobblify
402 wobblify False ty@(TyVarTy tv)
403 | isMetaTyVar tv = return ty -- Already wobbly
405 wobblify False ty = do { uniq <- newUnique
406 ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
409 ; return (mkTyVarTy tv) }
413 %************************************************************************
415 \subsection{Subsumption}
417 %************************************************************************
419 All the tcSub calls have the form
421 tcSub expected_ty offered_ty
423 offered_ty <= expected_ty
425 That is, that a value of type offered_ty is acceptable in
426 a place expecting a value of type expected_ty.
428 It returns a coercion function
429 co_fn :: offered_ty -> expected_ty
430 which takes an HsExpr of type offered_ty into one of type
434 -----------------------
435 -- tcSubExp is used for expressions
436 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
438 tcSubExp (Infer hole) offered_ty
439 = do { offered' <- zonkTcType offered_ty
440 -- Note [Zonk return type]
441 -- zonk to take advantage of the current GADT type refinement.
442 -- If we don't we get spurious "existential type variable escapes":
443 -- case (x::Maybe a) of
444 -- Just b (y::b) -> y
445 -- We need the refinement [b->a] to be applied to the result type
446 ; writeMutVar hole offered'
447 ; return idCoercion }
449 tcSubExp (Check expected_ty) offered_ty
450 = tcSub expected_ty offered_ty
452 -----------------------
453 -- tcSubPat is used for patterns
454 tcSubPat :: TcSigmaType -- Pattern type signature
455 -> Expected TcSigmaType -- Type from context
457 -- In patterns we insist on an exact match; hence no CoFn returned
458 -- See Note [Pattern coercions] in TcPat
459 -- However, we can't call unify directly, because both types might be
460 -- polymorphic; hence the call to tcSub, followed by a check for
461 -- equal types. (We can't just check for the identity coercion, because
462 -- in the polymorphic case we might get back something eta-equivalent to
463 -- the identity coercion, but that's not easy to tell.)
465 tcSubPat sig_ty (Infer hole)
466 = do { sig_ty' <- zonkTcType sig_ty
467 ; writeMutVar hole sig_ty' -- See notes with tcSubExp above
470 -- This tcSub followed by tcEqType checks for identical types
471 -- It'd be done more neatly by augmenting the unifier to deal with
472 -- (identically shaped) for-all types.
474 tcSubPat sig_ty (Check exp_ty)
475 = do { co_fn <- tcSub sig_ty exp_ty
476 ; sig_ty' <- zonkTcType sig_ty
477 ; exp_ty' <- zonkTcType exp_ty
478 ; if tcEqType sig_ty' exp_ty' then
481 { (env, msg) <- misMatchMsg sig_ty' exp_ty'
482 ; failWithTcM (env, msg $$ extra) } }
484 extra | isTauTy sig_ty = empty
485 | otherwise = ptext SLIT("Polymorphic types must match exactly in patterns")
490 %************************************************************************
492 tcSub: main subsumption-check code
494 %************************************************************************
496 No holes expected now. Add some error-check context info.
500 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
501 -- tcSub exp act checks that
503 tcSub expected_ty actual_ty
504 = traceTc (text "tcSub" <+> details) `thenM_`
505 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
506 (tc_sub expected_ty expected_ty actual_ty actual_ty)
508 details = vcat [text "Expected:" <+> ppr expected_ty,
509 text "Actual: " <+> ppr actual_ty]
512 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
513 -> TcSigmaType -- ..and after
514 -> TcSigmaType -- actual_ty, before
515 -> TcSigmaType -- ..and after
518 -----------------------------------
520 tc_sub exp_sty exp_ty act_sty act_ty
521 | Just exp_ty' <- tcView exp_ty = tc_sub exp_sty exp_ty' act_sty act_ty
522 tc_sub exp_sty exp_ty act_sty act_ty
523 | Just act_ty' <- tcView act_ty = tc_sub exp_sty exp_ty act_sty act_ty'
525 -----------------------------------
526 -- Generalisation case
527 -- actual_ty: d:Eq b => b->b
528 -- expected_ty: forall a. Ord a => a->a
529 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
531 -- It is essential to do this *before* the specialisation case
532 -- Example: f :: (Eq a => a->a) -> ...
533 -- g :: Ord b => b->b
536 tc_sub exp_sty expected_ty act_sty actual_ty
537 | isSigmaTy expected_ty
538 = tcGen expected_ty (tyVarsOfType actual_ty) (
539 -- It's really important to check for escape wrt the free vars of
540 -- both expected_ty *and* actual_ty
541 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
542 ) `thenM` \ (gen_fn, co_fn) ->
543 returnM (gen_fn <.> co_fn)
545 -----------------------------------
546 -- Specialisation case:
547 -- actual_ty: forall a. Ord a => a->a
548 -- expected_ty: Int -> Int
549 -- co_fn e = e Int dOrdInt
551 tc_sub exp_sty expected_ty act_sty actual_ty
552 | isSigmaTy actual_ty
553 = tcInstCall InstSigOrigin actual_ty `thenM` \ (inst_fn, _, body_ty) ->
554 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
555 returnM (co_fn <.> inst_fn)
557 -----------------------------------
560 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
561 = tcSub_fun exp_arg exp_res act_arg act_res
563 -----------------------------------
564 -- Type variable meets function: imitate
566 -- NB 1: we can't just unify the type variable with the type
567 -- because the type might not be a tau-type, and we aren't
568 -- allowed to instantiate an ordinary type variable with
571 -- NB 2: can we short-cut to an error case?
572 -- when the arg/res is not a tau-type?
573 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
575 -- is perfectly fine, because we can instantiate f's type to a monotype
577 -- However, we get can get jolly unhelpful error messages.
578 -- e.g. foo = id runST
580 -- Inferred type is less polymorphic than expected
581 -- Quantified type variable `s' escapes
582 -- Expected type: ST s a -> t
583 -- Inferred type: (forall s1. ST s1 a) -> a
584 -- In the first argument of `id', namely `runST'
585 -- In a right-hand side of function `foo': id runST
587 -- I'm not quite sure what to do about this!
589 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
590 = do { (act_arg, act_res) <- unify_fun act_ty
591 ; tcSub_fun exp_arg exp_res act_arg act_res }
593 tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
594 = do { (exp_arg, exp_res) <- unify_fun exp_ty
595 ; tcSub_fun exp_arg exp_res act_arg act_res }
597 -----------------------------------
599 -- If none of the above match, we revert to the plain unifier
600 tc_sub exp_sty expected_ty act_sty actual_ty
601 = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
604 -----------------------------------
605 -- A helper to make a function type match
606 -- The error message isn't very good, but that's a problem with
607 -- all of this subsumption code
609 = do { (ok, args, res) <- unify_fun_ty True 1 ty
610 ; if ok then return (head args, res)
611 else failWithTc (ptext SLIT("Expecting a function type, but found") <+> quotes (ppr ty))}
615 tcSub_fun exp_arg exp_res act_arg act_res
616 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
617 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
618 newUnique `thenM` \ uniq ->
620 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
621 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
622 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
623 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
624 coercion | isIdCoercion co_fn_arg,
625 isIdCoercion co_fn_res = idCoercion
626 | otherwise = mkCoercion co_fn
628 co_fn e = DictLam [arg_id]
629 (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
630 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
631 -- HsVar arg_id :: HsExpr exp_arg
632 -- co_fn_arg $it :: HsExpr act_arg
633 -- HsApp e $it :: HsExpr act_res
634 -- co_fn_res $it :: HsExpr exp_res
640 %************************************************************************
642 \subsection{Generalisation}
644 %************************************************************************
647 tcGen :: TcSigmaType -- expected_ty
648 -> TcTyVarSet -- Extra tyvars that the universally
649 -- quantified tyvars of expected_ty
650 -- must not be unified
651 -> (TcRhoType -> TcM result) -- spec_ty
652 -> TcM (ExprCoFn, result)
653 -- The expression has type: spec_ty -> expected_ty
655 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
656 -- If not, the call is a no-op
657 = do { -- We want the GenSkol info in the skolemised type variables to
658 -- mention the *instantiated* tyvar names, so that we get a
659 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
660 -- Hence the tiresome but innocuous fixM
661 ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
662 do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
663 ; span <- getSrcSpanM
664 ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
665 ; return ((forall_tvs, theta, rho_ty), skol_info) })
668 ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
669 text "expected_ty" <+> ppr expected_ty,
670 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
671 text "free_tvs" <+> ppr free_tvs,
672 text "forall_tvs" <+> ppr forall_tvs])
675 -- Type-check the arg and unify with poly type
676 ; (result, lie) <- getLIE (thing_inside rho_ty)
678 -- Check that the "forall_tvs" havn't been constrained
679 -- The interesting bit here is that we must include the free variables
680 -- of the expected_ty. Here's an example:
681 -- runST (newVar True)
682 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
683 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
684 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
685 -- So now s' isn't unconstrained because it's linked to a.
686 -- Conclusion: include the free vars of the expected_ty in the
687 -- list of "free vars" for the signature check.
689 ; dicts <- newDicts (SigOrigin skol_info) theta
690 ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
692 ; checkSigTyVarsWrt free_tvs forall_tvs
693 ; traceTc (text "tcGen:done")
696 -- This HsLet binds any Insts which came out of the simplification.
697 -- It's a bit out of place here, but using AbsBind involves inventing
698 -- a couple of new names which seems worse.
699 dict_ids = map instToId dicts
700 co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsDictLet inst_binds (noLoc e)))
701 ; returnM (mkCoercion co_fn, result) }
703 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
704 sig_msg = ptext SLIT("expected type of an expression")
709 %************************************************************************
711 \subsection[Unify-exported]{Exported unification functions}
713 %************************************************************************
715 The exported functions are all defined as versions of some
716 non-exported generic functions.
718 Unify two @TauType@s. Dead straightforward.
721 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
722 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
723 = -- The unifier should only ever see tau-types
724 -- (no quantification whatsoever)
725 ASSERT2( isTauTy ty1, ppr ty1 )
726 ASSERT2( isTauTy ty2, ppr ty2 )
727 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
728 uTys True ty1 ty1 True ty2 ty2
730 unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
731 unifyTheta theta1 theta2
732 = do { checkTc (equalLength theta1 theta2)
733 (ptext SLIT("Contexts differ in length"))
734 ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
737 @unifyTauTyList@ unifies corresponding elements of two lists of
738 @TauType@s. It uses @uTys@ to do the real work. The lists should be
739 of equal length. We charge down the list explicitly so that we can
740 complain if their lengths differ.
743 unifyTauTyLists :: Bool -> -- Allow refinements on tys1
745 Bool -> -- Allow refinements on tys2
746 [TcTauType] -> TcM ()
747 -- Precondition: lists must be same length
748 -- Having the caller check gives better error messages
749 -- Actually the caller neve does need to check; see Note [Tycon app]
750 unifyTauTyLists r1 [] r2 [] = returnM ()
751 unifyTauTyLists r1 (ty1:tys1) r2 (ty2:tys2) = uTys r1 ty1 ty1 r2 ty2 ty2 `thenM_`
752 unifyTauTyLists r1 tys1 r2 tys2
753 unifyTauTyLists r1 ty1s r2 ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
756 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
757 all together. It is used, for example, when typechecking explicit
758 lists, when all the elts should be of the same type.
761 unifyTauTyList :: [TcTauType] -> TcM ()
762 unifyTauTyList [] = returnM ()
763 unifyTauTyList [ty] = returnM ()
764 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
768 %************************************************************************
770 \subsection[Unify-uTys]{@uTys@: getting down to business}
772 %************************************************************************
774 @uTys@ is the heart of the unifier. Each arg happens twice, because
775 we want to report errors in terms of synomyms if poss. The first of
776 the pair is used in error messages only; it is always the same as the
777 second, except that if the first is a synonym then the second may be a
778 de-synonym'd version. This way we get better error messages.
780 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
783 uTys :: Bool -- Allow refinements to ty1
784 -> TcTauType -> TcTauType -- Error reporting ty1 and real ty1
785 -- ty1 is the *expected* type
786 -> Bool -- Allow refinements to ty2
787 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
788 -- ty2 is the *actual* type
791 -- Always expand synonyms (see notes at end)
792 -- (this also throws away FTVs)
793 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
794 | Just ty1' <- tcView ty1 = uTys r1 ps_ty1 ty1' r2 ps_ty2 ty2
795 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
796 | Just ty2' <- tcView ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2'
798 -- Variables; go for uVar
799 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
800 uTys r1 ps_ty1 ty1 r2 ps_ty2 (TyVarTy tyvar2) = uVar True r2 tyvar2 r1 ps_ty1 ty1
801 -- "True" means args swapped
804 uTys r1 _ (PredTy (IParam n1 t1)) r2 _ (PredTy (IParam n2 t2))
805 | n1 == n2 = uTys r1 t1 t1 r2 t2 t2
806 uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2))
807 | c1 == c2 = unifyTauTyLists r1 tys1 r2 tys2
808 -- Guaranteed equal lengths because the kinds check
810 -- Functions; just check the two parts
811 uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2)
812 = uTys r1 fun1 fun1 r2 fun2 fun2 `thenM_` uTys r1 arg1 arg1 r2 arg2 arg2
814 -- Type constructors must match
815 uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2)
816 | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2
817 -- See Note [TyCon app]
819 -- Applications need a bit of care!
820 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
821 -- NB: we've already dealt with type variables and Notes,
822 -- so if one type is an App the other one jolly well better be too
823 uTys r1 ps_ty1 (AppTy s1 t1) r2 ps_ty2 ty2
824 = case tcSplitAppTy_maybe ty2 of
825 Just (s2,t2) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
826 Nothing -> unifyMisMatch ps_ty1 ps_ty2
828 -- Now the same, but the other way round
829 -- Don't swap the types, because the error messages get worse
830 uTys r1 ps_ty1 ty1 r2 ps_ty2 (AppTy s2 t2)
831 = case tcSplitAppTy_maybe ty1 of
832 Just (s1,t1) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
833 Nothing -> unifyMisMatch ps_ty1 ps_ty2
835 -- Not expecting for-alls in unification
836 -- ... but the error message from the unifyMisMatch more informative
837 -- than a panic message!
839 -- Anything else fails
840 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
845 When we find two TyConApps, the argument lists are guaranteed equal
846 length. Reason: intially the kinds of the two types to be unified is
847 the same. The only way it can become not the same is when unifying two
848 AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
849 the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
850 which we do, that ensures that f1,f2 have the same kind; and that
851 means a1,a2 have the same kind. And now the argument repeats.
856 If you are tempted to make a short cut on synonyms, as in this
860 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
861 -- NO = if (con1 == con2) then
862 -- NO -- Good news! Same synonym constructors, so we can shortcut
863 -- NO -- by unifying their arguments and ignoring their expansions.
864 -- NO unifyTauTypeLists args1 args2
866 -- NO -- Never mind. Just expand them and try again
870 then THINK AGAIN. Here is the whole story, as detected and reported
871 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
873 Here's a test program that should detect the problem:
877 x = (1 :: Bogus Char) :: Bogus Bool
880 The problem with [the attempted shortcut code] is that
884 is not a sufficient condition to be able to use the shortcut!
885 You also need to know that the type synonym actually USES all
886 its arguments. For example, consider the following type synonym
887 which does not use all its arguments.
892 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
893 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
894 would fail, even though the expanded forms (both \tr{Int}) should
897 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
898 unnecessarily bind \tr{t} to \tr{Char}.
900 ... You could explicitly test for the problem synonyms and mark them
901 somehow as needing expansion, perhaps also issuing a warning to the
906 %************************************************************************
908 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
910 %************************************************************************
912 @uVar@ is called when at least one of the types being unified is a
913 variable. It does {\em not} assume that the variable is a fixed point
914 of the substitution; rather, notice that @uVar@ (defined below) nips
915 back into @uTys@ if it turns out that the variable is already bound.
918 uVar :: Bool -- False => tyvar is the "expected"
919 -- True => ty is the "expected" thing
920 -> Bool -- True, allow refinements to tv1, False don't
922 -> Bool -- Allow refinements to ty2?
923 -> TcTauType -> TcTauType -- printing and real versions
926 uVar swapped r1 tv1 r2 ps_ty2 ty2
927 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
928 condLookupTcTyVar r1 tv1 `thenM` \ details ->
930 IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
931 | otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
932 DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
935 uDoneVar :: Bool -- Args are swapped
936 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
937 -> Bool -- Allow refinements to ty2
938 -> TcTauType -> TcTauType -- Type 2
940 -- Invariant: tyvar 1 is not unified with anything
942 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
943 | Just ty2' <- tcView ty2
944 = -- Expand synonyms; ignore FTVs
945 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2'
947 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
948 -- Same type variable => no-op
952 -- Distinct type variables
954 = do { lookup2 <- condLookupTcTyVar r2 tv2
956 IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2'
957 DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2
960 uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
962 MetaTv ref1 -> do { -- Do the occurs check, and check that we are not
963 -- unifying a type variable with a polytype
964 -- Returns a zonked type ready for the update
965 ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
966 ; updateMeta swapped tv1 ref1 ty2 }
968 skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
972 uDoneVars :: Bool -- Args are swapped
973 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
974 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
976 -- Invarant: the type variables are distinct,
977 -- and are not already unified with anything
979 uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
981 MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
982 other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
983 -- Note that updateMeta does a sub-kind check
984 -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
988 update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
989 -- Update the variable with least kind info
990 -- See notes on type inference in Kind.lhs
991 -- The "nicer to" part only applies if the two kinds are the same,
992 -- so we can choose which to do.
994 nicer_to_update_tv2 = isSystemName (varName tv2)
995 -- Try to update sys-y type variables in preference to ones
996 -- gotten (say) by instantiating a polymorphic function with
997 -- a user-written type sig
999 uDoneVars swapped tv1 (SkolemTv _) tv2 details2
1001 MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
1002 other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
1004 uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
1006 MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
1007 SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
1008 other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
1011 updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
1012 -- Update tv1, which is flexi; occurs check is alrady done
1013 updateMeta swapped tv1 ref1 ty2
1014 = do { checkKinds swapped tv1 ty2
1015 ; writeMutVar ref1 (Indirect ty2) }
1019 checkKinds swapped tv1 ty2
1020 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1021 -- ty2 has been zonked at this stage, which ensures that
1022 -- its kind has as much boxity information visible as possible.
1023 | tk2 `isSubKind` tk1 = returnM ()
1026 -- Either the kinds aren't compatible
1027 -- (can happen if we unify (a b) with (c d))
1028 -- or we are unifying a lifted type variable with an
1029 -- unlifted type: e.g. (id 3#) is illegal
1030 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1031 unifyKindMisMatch k1 k2
1033 (k1,k2) | swapped = (tk2,tk1)
1034 | otherwise = (tk1,tk2)
1040 checkValue tv1 r2 ps_ty2 non_var_ty2
1041 -- Do the occurs check, and check that we are not
1042 -- unifying a type variable with a polytype
1043 -- Return the type to update the type variable with, or fail
1045 -- Basically we want to update tv1 := ps_ty2
1046 -- because ps_ty2 has type-synonym info, which improves later error messages
1051 -- f :: (A a -> a -> ()) -> ()
1055 -- x = f (\ x p -> p x)
1057 -- In the application (p x), we try to match "t" with "A t". If we go
1058 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1059 -- an infinite loop later.
1060 -- But we should not reject the program, because A t = ().
1061 -- Rather, we should bind t to () (= non_var_ty2).
1063 -- That's why we have this two-state occurs-check
1064 = zonk_tc_type r2 ps_ty2 `thenM` \ ps_ty2' ->
1065 case okToUnifyWith tv1 ps_ty2' of {
1066 Nothing -> returnM ps_ty2' ; -- Success
1069 zonk_tc_type r2 non_var_ty2 `thenM` \ non_var_ty2' ->
1070 case okToUnifyWith tv1 non_var_ty2' of
1071 Nothing -> -- This branch rarely succeeds, except in strange cases
1072 -- like that in the example above
1073 returnM non_var_ty2'
1075 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
1078 zonk_tc_type refine ty
1079 = zonkType (\tv -> return (TyVarTy tv)) refine ty
1080 -- We may already be inside a wobbly type t2, and
1081 -- should take that into account here
1083 data Problem = OccurCheck | NotMonoType
1085 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
1086 -- (okToUnifyWith tv ty) checks whether it's ok to unify
1089 -- Just p => not ok, problem p
1094 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
1095 | otherwise = Nothing
1096 ok (AppTy t1 t2) = ok t1 `and` ok t2
1097 ok (FunTy t1 t2) = ok t1 `and` ok t2
1098 ok (TyConApp tc ts) = oks ts `and` ok_syn tc
1099 ok (ForAllTy _ _) = Just NotMonoType
1100 ok (PredTy st) = ok_st st
1101 ok (NoteTy _ t) = ok t
1103 oks ts = foldr (and . ok) Nothing ts
1105 ok_st (ClassP _ ts) = oks ts
1106 ok_st (IParam _ t) = ok t
1108 -- Check that a type synonym doesn't have a forall in the RHS
1109 ok_syn tc | not (isSynTyCon tc) = Nothing
1110 | otherwise = ok (snd (getSynTyConDefn tc))
1113 Just p `and` m = Just p
1117 %************************************************************************
1121 %************************************************************************
1123 Unifying kinds is much, much simpler than unifying types.
1126 unifyKind :: TcKind -- Expected
1129 unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
1130 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
1132 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
1133 unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
1134 -- Respect sub-kinding
1136 unifyKind (FunKind a1 r1) (FunKind a2 r2)
1137 = do { unifyKind a2 a1; unifyKind r1 r2 }
1138 -- Notice the flip in the argument,
1139 -- so that the sub-kinding works right
1141 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
1142 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
1143 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1145 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1146 unifyKinds [] [] = returnM ()
1147 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
1149 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1152 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1153 uKVar swapped kv1 k2
1154 = do { mb_k1 <- readKindVar kv1
1156 Nothing -> uUnboundKVar swapped kv1 k2
1157 Just k1 | swapped -> unifyKind k2 k1
1158 | otherwise -> unifyKind k1 k2 }
1161 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1162 uUnboundKVar swapped kv1 k2@(KindVar kv2)
1163 | kv1 == kv2 = returnM ()
1164 | otherwise -- Distinct kind variables
1165 = do { mb_k2 <- readKindVar kv2
1167 Just k2 -> uUnboundKVar swapped kv1 k2
1168 Nothing -> writeKindVar kv1 k2 }
1170 uUnboundKVar swapped kv1 non_var_k2
1171 = do { k2' <- zonkTcKind non_var_k2
1172 ; kindOccurCheck kv1 k2'
1173 ; k2'' <- kindSimpleKind swapped k2'
1174 -- KindVars must be bound only to simple kinds
1175 -- Polarities: (kindSimpleKind True ?) succeeds
1176 -- returning *, corresponding to unifying
1179 ; writeKindVar kv1 k2'' }
1182 kindOccurCheck kv1 k2 -- k2 is zonked
1183 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1185 not_in (KindVar kv2) = kv1 /= kv2
1186 not_in (FunKind a2 r2) = not_in a2 && not_in r2
1189 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1190 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1191 -- If the flag is False, it requires k <: sk
1192 -- E.g. kindSimpleKind False ?? = *
1193 -- What about (kv -> *) :=: ?? -> *
1194 kindSimpleKind orig_swapped orig_kind
1195 = go orig_swapped orig_kind
1197 go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
1199 ; return (FunKind k1' k2') }
1200 go True OpenTypeKind = return liftedTypeKind
1201 go True ArgTypeKind = return liftedTypeKind
1202 go sw LiftedTypeKind = return liftedTypeKind
1203 go sw k@(KindVar _) = return k -- KindVars are always simple
1204 go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1205 <+> ppr orig_swapped <+> ppr orig_kind)
1206 -- I think this can't actually happen
1208 -- T v = MkT v v must be a type
1209 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1212 kindOccurCheckErr tyvar ty
1213 = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1214 2 (sep [ppr tyvar, char '=', ppr ty])
1216 unifyKindMisMatch ty1 ty2
1217 = zonkTcKind ty1 `thenM` \ ty1' ->
1218 zonkTcKind ty2 `thenM` \ ty2' ->
1220 msg = hang (ptext SLIT("Couldn't match kind"))
1221 2 (sep [quotes (ppr ty1'),
1222 ptext SLIT("against"),
1229 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1230 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1232 unifyFunKind (KindVar kvar)
1233 = readKindVar kvar `thenM` \ maybe_kind ->
1235 Just fun_kind -> unifyFunKind fun_kind
1236 Nothing -> do { arg_kind <- newKindVar
1237 ; res_kind <- newKindVar
1238 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1239 ; returnM (Just (arg_kind,res_kind)) }
1241 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1242 unifyFunKind other = returnM Nothing
1245 %************************************************************************
1247 \subsection[Unify-context]{Errors and contexts}
1249 %************************************************************************
1255 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1256 = zonkTcType ty1 `thenM` \ ty1' ->
1257 zonkTcType ty2 `thenM` \ ty2' ->
1258 returnM (err ty1' ty2')
1260 err ty1 ty2 = (env1,
1263 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1264 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1267 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1269 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1270 -- tv1 and ty2 are zonked already
1273 msg = (env2, ptext SLIT("When matching the kinds of") <+>
1274 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1276 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1277 | otherwise = (pp1, pp2)
1278 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1279 (env2, ty2') = tidyOpenType env1 ty2
1280 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1281 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1283 unifyMisMatch ty1 ty2
1284 = do { (env, msg) <- misMatchMsg ty1 ty2
1285 ; failWithTcM (env, msg) }
1288 = do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
1289 ; (env2, pp2, extra2) <- ppr_ty env1 ty2
1290 ; return (env2, sep [sep [ptext SLIT("Couldn't match") <+> pp1,
1291 nest 7 (ptext SLIT("against") <+> pp2)],
1292 nest 2 extra1, nest 2 extra2]) }
1294 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1296 = do { ty' <- zonkTcType ty
1297 ; let (env1,tidy_ty) = tidyOpenType env ty'
1298 simple_result = (env1, quotes (ppr tidy_ty), empty)
1301 | isSkolemTyVar tv -> return (env2, pp_rigid tv',
1303 | otherwise -> return simple_result
1305 (env2, tv') = tidySkolemTyVar env1 tv
1306 other -> return simple_result }
1308 pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
1310 unifyCheck problem tyvar ty
1312 2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1314 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1315 (env2, tidy_ty) = tidyOpenType env1 ty
1317 msg = case problem of
1318 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1319 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1323 %************************************************************************
1327 %************************************************************************
1329 ---------------------------
1330 -- We would like to get a decent error message from
1331 -- (a) Under-applied type constructors
1332 -- f :: (Maybe, Maybe)
1333 -- (b) Over-applied type constructors
1334 -- f :: Int x -> Int x
1338 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1339 -- A fancy wrapper for 'unifyKind', which tries
1340 -- to give decent error messages.
1341 checkExpectedKind ty act_kind exp_kind
1342 | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1345 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
1347 Just r -> returnM () ; -- Unification succeeded
1350 -- So there's definitely an error
1351 -- Now to find out what sort
1352 zonkTcKind exp_kind `thenM` \ exp_kind ->
1353 zonkTcKind act_kind `thenM` \ act_kind ->
1355 let (exp_as, _) = splitKindFunTys exp_kind
1356 (act_as, _) = splitKindFunTys act_kind
1357 n_exp_as = length exp_as
1358 n_act_as = length act_as
1360 (env1, tidy_exp_kind) = tidyKind emptyTidyEnv exp_kind
1361 (env2, tidy_act_kind) = tidyKind env1 act_kind
1363 err | n_exp_as < n_act_as -- E.g. [Maybe]
1364 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1366 -- Now n_exp_as >= n_act_as. In the next two cases,
1367 -- n_exp_as == 0, and hence so is n_act_as
1368 | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1369 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1370 <+> ptext SLIT("is unlifted")
1372 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1373 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1374 <+> ptext SLIT("is lifted")
1376 | otherwise -- E.g. Monad [Int]
1377 = ptext SLIT("Kind mis-match")
1379 more_info = sep [ ptext SLIT("Expected kind") <+>
1380 quotes (pprKind tidy_exp_kind) <> comma,
1381 ptext SLIT("but") <+> quotes (ppr ty) <+>
1382 ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
1384 failWithTcM (env2, err $$ more_info)
1388 %************************************************************************
1390 \subsection{Checking signature type variables}
1392 %************************************************************************
1394 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1395 are not mentioned in the environment. In particular:
1397 (a) Not mentioned in the type of a variable in the envt
1398 eg the signature for f in this:
1404 Here, f is forced to be monorphic by the free occurence of x.
1406 (d) Not (unified with another type variable that is) in scope.
1407 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1408 when checking the expression type signature, we find that
1409 even though there is nothing in scope whose type mentions r,
1410 nevertheless the type signature for the expression isn't right.
1412 Another example is in a class or instance declaration:
1414 op :: forall b. a -> b
1416 Here, b gets unified with a
1418 Before doing this, the substitution is applied to the signature type variable.
1421 checkSigTyVars :: [TcTyVar] -> TcM ()
1422 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1424 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1425 checkSigTyVarsWrt extra_tvs sig_tvs
1426 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1427 check_sig_tyvars extra_tvs' sig_tvs
1430 :: TcTyVarSet -- Global type variables. The universally quantified
1431 -- tyvars should not mention any of these
1432 -- Guaranteed already zonked.
1433 -> [TcTyVar] -- Universally-quantified type variables in the signature
1434 -- Guaranteed to be skolems
1436 check_sig_tyvars extra_tvs []
1438 check_sig_tyvars extra_tvs sig_tvs
1439 = ASSERT( all isSkolemTyVar sig_tvs )
1440 do { gbl_tvs <- tcGetGlobalTyVars
1441 ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1442 text "gbl_tvs" <+> ppr gbl_tvs,
1443 text "extra_tvs" <+> ppr extra_tvs]))
1445 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1446 ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
1447 (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1450 bleatEscapedTvs :: TcTyVarSet -- The global tvs
1451 -> [TcTyVar] -- The possibly-escaping type variables
1452 -> [TcTyVar] -- The zonked versions thereof
1454 -- Complain about escaping type variables
1455 -- We pass a list of type variables, at least one of which
1456 -- escapes. The first list contains the original signature type variable,
1457 -- while the second contains the type variable it is unified to (usually itself)
1458 bleatEscapedTvs globals sig_tvs zonked_tvs
1459 = do { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1460 ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1462 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1463 (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1465 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1467 check (tidy_env, msgs) (sig_tv, zonked_tv)
1468 | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1470 = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
1471 ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1473 -----------------------
1474 escape_msg sig_tv zonked_tv globs
1476 = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
1477 nest 2 (vcat globs)]
1479 = msg <+> ptext SLIT("escapes")
1480 -- Sigh. It's really hard to give a good error message
1481 -- all the time. One bad case is an existential pattern match.
1482 -- We rely on the "When..." context to help.
1484 msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1486 | sig_tv == zonked_tv = empty
1487 | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
1490 These two context are used with checkSigTyVars
1493 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1494 -> TidyEnv -> TcM (TidyEnv, Message)
1495 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1496 = zonkTcType sig_tau `thenM` \ actual_tau ->
1498 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1499 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1500 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1501 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1502 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1504 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),