Comments and white space; plus structurally avoiding the previously "egregious bug"
[ghc.git] / compiler / typecheck / TcUnify.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Type subsumption and unification
7 -}
8
9 {-# LANGUAGE CPP #-}
10
11 module TcUnify (
12 -- Full-blown subsumption
13 tcWrapResult, tcGen,
14 tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
15 checkConstraints,
16
17 -- Various unifications
18 unifyType, unifyTypeList, unifyTheta,
19 unifyKindX,
20
21 --------------------------------
22 -- Holes
23 tcInfer,
24 matchExpectedListTy,
25 matchExpectedPArrTy,
26 matchExpectedTyConApp,
27 matchExpectedAppTy,
28 matchExpectedFunTys,
29 matchExpectedFunKind,
30 wrapFunResCoercion
31
32 ) where
33
34 #include "HsVersions.h"
35
36 import HsSyn
37 import TypeRep
38 import TcMType
39 import TcRnMonad
40 import TcType
41 import Type
42 import TcEvidence
43 import Name ( isSystemName )
44 import Inst
45 import Kind
46 import TyCon
47 import TysWiredIn
48 import Var
49 import VarEnv
50 import VarSet
51 import ErrUtils
52 import DynFlags
53 import BasicTypes
54 import Maybes ( isJust )
55 import Util
56 import Outputable
57 import FastString
58
59 import Control.Monad
60
61 {-
62 ************************************************************************
63 * *
64 matchExpected functions
65 * *
66 ************************************************************************
67
68 Note [Herald for matchExpectedFunTys]
69 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
70 The 'herald' always looks like:
71 "The equation(s) for 'f' have"
72 "The abstraction (\x.e) takes"
73 "The section (+ x) expects"
74 "The function 'f' is applied to"
75
76 This is used to construct a message of form
77
78 The abstraction `\Just 1 -> ...' takes two arguments
79 but its type `Maybe a -> a' has only one
80
81 The equation(s) for `f' have two arguments
82 but its type `Maybe a -> a' has only one
83
84 The section `(f 3)' requires 'f' to take two arguments
85 but its type `Int -> Int' has only one
86
87 The function 'f' is applied to two arguments
88 but its type `Int -> Int' has only one
89
90 Note [matchExpectedFunTys]
91 ~~~~~~~~~~~~~~~~~~~~~~~~~~
92 matchExpectedFunTys checks that an (Expected rho) has the form
93 of an n-ary function. It passes the decomposed type to the
94 thing_inside, and returns a wrapper to coerce between the two types
95
96 It's used wherever a language construct must have a functional type,
97 namely:
98 A lambda expression
99 A function definition
100 An operator section
101
102 This is not (currently) where deep skolemisation occurs;
103 matchExpectedFunTys does not skolmise nested foralls in the
104 expected type, because it expects that to have been done already
105 -}
106
107 matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
108 -> Arity
109 -> TcRhoType
110 -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
111
112 -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
113 -- then co : ty ~ (t1 -> ... -> tn -> ty_r)
114 --
115 -- Does not allocate unnecessary meta variables: if the input already is
116 -- a function, we just take it apart. Not only is this efficient,
117 -- it's important for higher rank: the argument might be of form
118 -- (forall a. ty) -> other
119 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
120 -- hide the forall inside a meta-variable
121
122 matchExpectedFunTys herald arity orig_ty
123 = go arity orig_ty
124 where
125 -- If go n ty = (co, [t1,..,tn], ty_r)
126 -- then co : ty ~ t1 -> .. -> tn -> ty_r
127
128 go n_req ty
129 | n_req == 0 = return (mkTcNomReflCo ty, [], ty)
130
131 go n_req ty
132 | Just ty' <- tcView ty = go n_req ty'
133
134 go n_req (FunTy arg_ty res_ty)
135 | not (isPredTy arg_ty)
136 = do { (co, tys, ty_r) <- go (n_req-1) res_ty
137 ; return (mkTcFunCo Nominal (mkTcNomReflCo arg_ty) co, arg_ty:tys, ty_r) }
138
139 go n_req ty@(TyVarTy tv)
140 | ASSERT( isTcTyVar tv) isMetaTyVar tv
141 = do { cts <- readMetaTyVar tv
142 ; case cts of
143 Indirect ty' -> go n_req ty'
144 Flexi -> defer n_req ty (isReturnTyVar tv) }
145
146 -- In all other cases we bale out into ordinary unification
147 -- However unlike the meta-tyvar case, we are sure that the
148 -- number of arguments doesn't match arity of the original
149 -- type, so we can add a bit more context to the error message
150 -- (cf Trac #7869).
151 --
152 -- It is not always an error, because specialized type may have
153 -- different arity, for example:
154 --
155 -- > f1 = f2 'a'
156 -- > f2 :: Monad m => m Bool
157 -- > f2 = undefined
158 --
159 -- But in that case we add specialized type into error context
160 -- anyway, because it may be useful. See also Trac #9605.
161 go n_req ty = addErrCtxtM mk_ctxt $
162 defer n_req ty False
163
164 ------------
165 -- If we decide that a ReturnTv (see Note [ReturnTv] in TcType) should
166 -- really be a function type, then we need to allow the argument and
167 -- result types also to be ReturnTvs.
168 defer n_req fun_ty is_return
169 = do { arg_tys <- mapM new_ty_var_ty (nOfThem n_req openTypeKind)
170 -- See Note [Foralls to left of arrow]
171 ; res_ty <- new_ty_var_ty openTypeKind
172 ; co <- unifyType fun_ty (mkFunTys arg_tys res_ty)
173 ; return (co, arg_tys, res_ty) }
174 where
175 new_ty_var_ty | is_return = newReturnTyVarTy
176 | otherwise = newFlexiTyVarTy
177
178 ------------
179 mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
180 mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_ty
181 ; let (args, _) = tcSplitFunTys ty
182 n_actual = length args
183 (env'', orig_ty') = tidyOpenType env' orig_ty
184 ; return (env'', mk_msg orig_ty' ty n_actual) }
185
186 mk_msg orig_ty ty n_args
187 = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
188 if n_args == arity
189 then ptext (sLit "its type is") <+> quotes (pprType orig_ty) <>
190 comma $$
191 ptext (sLit "it is specialized to") <+> quotes (pprType ty)
192 else sep [ptext (sLit "but its type") <+> quotes (pprType ty),
193 if n_args == 0 then ptext (sLit "has none")
194 else ptext (sLit "has only") <+> speakN n_args]
195
196 {-
197 Note [Foralls to left of arrow]
198 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
199 Consider
200 f (x :: forall a. a -> a) = x
201 We give 'f' the type (alpha -> beta), and then want to unify
202 the alpha with (forall a. a->a). We want to the arg and result
203 of (->) to have openTypeKind, and this also permits foralls, so
204 we are ok.
205 -}
206
207 ----------------------
208 matchExpectedListTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
209 -- Special case for lists
210 matchExpectedListTy exp_ty
211 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
212 ; return (co, elt_ty) }
213
214 ----------------------
215 matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
216 -- Special case for parrs
217 matchExpectedPArrTy exp_ty
218 = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
219 ; return (co, elt_ty) }
220
221 ---------------------
222 matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
223 -> TcRhoType -- orig_ty
224 -> TcM (TcCoercion, -- T k1 k2 k3 a b c ~ orig_ty
225 [TcSigmaType]) -- Element types, k1 k2 k3 a b c
226
227 -- It's used for wired-in tycons, so we call checkWiredInTyCon
228 -- Precondition: never called with FunTyCon
229 -- Precondition: input type :: *
230 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
231
232 matchExpectedTyConApp tc orig_ty
233 = go orig_ty
234 where
235 go ty
236 | Just ty' <- tcView ty
237 = go ty'
238
239 go ty@(TyConApp tycon args)
240 | tc == tycon -- Common case
241 = return (mkTcNomReflCo ty, args)
242
243 go (TyVarTy tv)
244 | ASSERT( isTcTyVar tv) isMetaTyVar tv
245 = do { cts <- readMetaTyVar tv
246 ; case cts of
247 Indirect ty -> go ty
248 Flexi -> defer }
249
250 go _ = defer
251
252 -- If the common case does not occur, instantiate a template
253 -- T k1 .. kn t1 .. tm, and unify with the original type
254 -- Doing it this way ensures that the types we return are
255 -- kind-compatible with T. For example, suppose we have
256 -- matchExpectedTyConApp T (f Maybe)
257 -- where data T a = MkT a
258 -- Then we don't want to instantate T's data constructors with
259 -- (a::*) ~ Maybe
260 -- because that'll make types that are utterly ill-kinded.
261 -- This happened in Trac #7368
262 defer = ASSERT2( isSubOpenTypeKind res_kind, ppr tc )
263 do { kappa_tys <- mapM (const newMetaKindVar) kvs
264 ; let arg_kinds' = map (substKiWith kvs kappa_tys) arg_kinds
265 ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
266 ; co <- unifyType (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty
267 ; return (co, kappa_tys ++ tau_tys) }
268
269 (kvs, body) = splitForAllTys (tyConKind tc)
270 (arg_kinds, res_kind) = splitKindFunTys body
271
272 ----------------------
273 matchExpectedAppTy :: TcRhoType -- orig_ty
274 -> TcM (TcCoercion, -- m a ~ orig_ty
275 (TcSigmaType, TcSigmaType)) -- Returns m, a
276 -- If the incoming type is a mutable type variable of kind k, then
277 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
278
279 matchExpectedAppTy orig_ty
280 = go orig_ty
281 where
282 go ty
283 | Just ty' <- tcView ty = go ty'
284
285 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
286 = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
287
288 go (TyVarTy tv)
289 | ASSERT( isTcTyVar tv) isMetaTyVar tv
290 = do { cts <- readMetaTyVar tv
291 ; case cts of
292 Indirect ty -> go ty
293 Flexi -> defer }
294
295 go _ = defer
296
297 -- Defer splitting by generating an equality constraint
298 defer = do { ty1 <- newFlexiTyVarTy kind1
299 ; ty2 <- newFlexiTyVarTy kind2
300 ; co <- unifyType (mkAppTy ty1 ty2) orig_ty
301 ; return (co, (ty1, ty2)) }
302
303 orig_kind = typeKind orig_ty
304 kind1 = mkArrowKind liftedTypeKind (defaultKind orig_kind)
305 kind2 = liftedTypeKind -- m :: * -> k
306 -- arg type :: *
307 -- The defaultKind is a bit smelly. If you remove it,
308 -- try compiling f x = do { x }
309 -- and you'll get a kind mis-match. It smells, but
310 -- not enough to lose sleep over.
311
312 {-
313 ************************************************************************
314 * *
315 Subsumption checking
316 * *
317 ************************************************************************
318
319 Note [Subsumption checking: tcSubType]
320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
321 All the tcSubType calls have the form
322 tcSubType actual_ty expected_ty
323 which checks
324 actual_ty <= expected_ty
325
326 That is, that a value of type actual_ty is acceptable in
327 a place expecting a value of type expected_ty. I.e. that
328
329 actual ty is more polymorphic than expected_ty
330
331 It returns a coercion function
332 co_fn :: actual_ty ~ expected_ty
333 which takes an HsExpr of type actual_ty into one of type
334 expected_ty.
335
336 There are a number of wrinkles (below).
337
338 Notice that Wrinkle 1 and 2 both require eta-expansion, which technically
339 may increase termination. We just put up with this, in exchange for getting
340 more predicatble type inference.
341
342 Wrinkle 1: Note [Deep skolemisation]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a)
345 (see section 4.6 of "Practical type inference for higher rank types")
346 So we must deeply-skolemise the RHS before we instantiate the LHS.
347
348 That is why tc_sub_type starts with a call to tcGen (which does the
349 deep skolemisation), and then calls the DS variant (which assumes
350 that expected_ty is deeply skolemised)
351
352 Wrinkle 2: Note [Co/contra-variance of subsumption checking]
353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 Consider g :: (Int -> Int) -> Int
355 f1 :: (forall a. a -> a) -> Int
356 f1 = g
357
358 f2 :: (forall a. a -> a) -> Int
359 f2 x = g x
360 f2 will typecheck, and it would be odd/fragile if f1 did not.
361 But f1 will only typecheck if we have that
362 (Int->Int) -> Int <= (forall a. a->a) -> Int
363 And that is only true if we do the full co/contravariant thing
364 in the subsumption check. That happens in the FunTy case of
365 tc_sub_type_ds, and is the sole reason for the WpFun form of
366 HsWrapper.
367
368 Another powerful reason for doing this co/contra stuff is visible
369 in Trac #9569, involving instantiation of constraint variables,
370 and again involving eta-expansion.
371
372 Wrinkle 3: Note [Higher rank types]
373 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
374 Consider tc150:
375 f y = \ (x::forall a. a->a). blah
376 The following happens:
377 * We will infer the type of the RHS, ie with a res_ty = alpha.
378 * Then the lambda will split alpha := beta -> gamma.
379 * And then we'll check tcSubType IsSwapped beta (forall a. a->a)
380
381 So it's important that we unify beta := forall a. a->a, rather than
382 skolemising the type.
383 -}
384
385 tcSubType :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
386 -- Checks that actual <= expected
387 -- Returns HsWrapper :: actual ~ expected
388 tcSubType ctxt ty_actual ty_expected
389 = addSubTypeCtxt ty_actual ty_expected $
390 tcSubType_NC ctxt ty_actual ty_expected
391
392 tcSubTypeDS :: UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
393 -- Just like tcSubType, but with the additional precondition that
394 -- ty_expected is deeply skolemised (hence "DS")
395 tcSubTypeDS ctxt ty_actual ty_expected
396 = addSubTypeCtxt ty_actual ty_expected $
397 tcSubTypeDS_NC ctxt ty_actual ty_expected
398
399
400 addSubTypeCtxt :: TcType -> TcType -> TcM a -> TcM a
401 addSubTypeCtxt ty_actual ty_expected thing_inside
402 | isRhoTy ty_actual -- If there is no polymorphism involved, the
403 , isRhoTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions)
404 = thing_inside -- gives enough context by itself
405 | otherwise
406 = addErrCtxtM mk_msg thing_inside
407 where
408 mk_msg tidy_env
409 = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual
410 ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
411 ; let msg = vcat [ hang (ptext (sLit "When checking that:"))
412 4 (ppr ty_actual)
413 , nest 2 (hang (ptext (sLit "is more polymorphic than:"))
414 2 (ppr ty_expected)) ]
415 ; return (tidy_env, msg) }
416
417 ---------------
418 -- The "_NC" variants do not add a typechecker-error context;
419 -- the caller is assumed to do that
420
421 tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
422 tcSubType_NC ctxt ty_actual ty_expected
423 = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
424 ; tc_sub_type origin ctxt ty_actual ty_expected }
425 where
426 origin = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected }
427
428 tcSubTypeDS_NC :: UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
429 tcSubTypeDS_NC ctxt ty_actual ty_expected
430 = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
431 ; tc_sub_type_ds origin ctxt ty_actual ty_expected }
432 where
433 origin = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected }
434
435 ---------------
436 tc_sub_type :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
437 tc_sub_type origin ctxt ty_actual ty_expected
438 | isTyVarTy ty_actual -- See Note [Higher rank types]
439 = do { cow <- uType origin ty_actual ty_expected
440 ; return (coToHsWrapper cow) }
441
442 | otherwise -- See Note [Deep skolemisation]
443 = do { (sk_wrap, inner_wrap) <- tcGen ctxt ty_expected $ \ _ sk_rho ->
444 tc_sub_type_ds origin ctxt ty_actual sk_rho
445 ; return (sk_wrap <.> inner_wrap) }
446
447 ---------------
448 tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
449 -- Just like tcSubType, but with the additional precondition that
450 -- ty_expected is deeply skolemised
451 tc_sub_type_ds origin ctxt ty_actual ty_expected
452 | Just (act_arg, act_res) <- tcSplitFunTy_maybe ty_actual
453 , Just (exp_arg, exp_res) <- tcSplitFunTy_maybe ty_expected
454 = -- See Note [Co/contra-variance of subsumption checking]
455 do { res_wrap <- tc_sub_type_ds origin ctxt act_res exp_res
456 ; arg_wrap <- tc_sub_type origin ctxt exp_arg act_arg
457 ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
458 -- arg_wrap :: exp_arg ~ act_arg
459 -- res_wrap :: act-res ~ exp_res
460
461 | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual
462 , not (null tvs && null theta)
463 = do { (subst, tvs') <- tcInstTyVars tvs
464 ; let tys' = mkTyVarTys tvs'
465 theta' = substTheta subst theta
466 in_rho' = substTy subst in_rho
467 ; in_wrap <- instCall origin tys' theta'
468 ; body_wrap <- tcSubTypeDS_NC ctxt in_rho' ty_expected
469 ; return (body_wrap <.> in_wrap) }
470
471 | otherwise -- Revert to unification
472 = do { cow <- uType origin ty_actual ty_expected
473 ; return (coToHsWrapper cow) }
474
475 -----------------
476 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
477 tcWrapResult expr actual_ty res_ty
478 = do { cow <- tcSubTypeDS GenSigCtxt actual_ty res_ty
479 -- Both types are deeply skolemised
480 ; return (mkHsWrap cow expr) }
481
482 -----------------------------------
483 wrapFunResCoercion
484 :: [TcType] -- Type of args
485 -> HsWrapper -- HsExpr a -> HsExpr b
486 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
487 wrapFunResCoercion arg_tys co_fn_res
488 | isIdHsWrapper co_fn_res
489 = return idHsWrapper
490 | null arg_tys
491 = return co_fn_res
492 | otherwise
493 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
494 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
495
496 -----------------------------------
497 -- | Infer a type using a type "checking" function by passing in a ReturnTv,
498 -- which can unify with *anything*. See also Note [ReturnTv] in TcType
499 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
500 tcInfer tc_check
501 = do { ret_tv <- newReturnTyVar openTypeKind
502 ; res <- tc_check (mkTyVarTy ret_tv)
503 ; details <- readMetaTyVar ret_tv
504 ; res_ty <- case details of
505 Indirect ty -> return ty
506 Flexi -> -- Checking was uninformative
507 do { traceTc "Defaulting un-filled ReturnTv to a TauTv" (ppr ret_tv)
508 ; tau_ty <- newFlexiTyVarTy openTypeKind
509 ; writeMetaTyVar ret_tv tau_ty
510 ; return tau_ty }
511 ; return (res, res_ty) }
512
513 {-
514 ************************************************************************
515 * *
516 \subsection{Generalisation}
517 * *
518 ************************************************************************
519 -}
520
521 tcGen :: UserTypeCtxt -> TcType
522 -> ([TcTyVar] -> TcRhoType -> TcM result)
523 -> TcM (HsWrapper, result)
524 -- The expression has type: spec_ty -> expected_ty
525
526 tcGen ctxt expected_ty thing_inside
527 -- We expect expected_ty to be a forall-type
528 -- If not, the call is a no-op
529 = do { traceTc "tcGen" Outputable.empty
530 ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
531
532 ; when debugIsOn $
533 traceTc "tcGen" $ vcat [
534 text "expected_ty" <+> ppr expected_ty,
535 text "inst ty" <+> ppr tvs' <+> ppr rho' ]
536
537 -- Generally we must check that the "forall_tvs" havn't been constrained
538 -- The interesting bit here is that we must include the free variables
539 -- of the expected_ty. Here's an example:
540 -- runST (newVar True)
541 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
542 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
543 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
544 -- So now s' isn't unconstrained because it's linked to a.
545 --
546 -- However [Oct 10] now that the untouchables are a range of
547 -- TcTyVars, all this is handled automatically with no need for
548 -- extra faffing around
549
550 -- Use the *instantiated* type in the SkolemInfo
551 -- so that the names of displayed type variables line up
552 ; let skol_info = SigSkol ctxt (mkPiTypes given rho')
553
554 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
555 thing_inside tvs' rho'
556
557 ; return (wrap <.> mkWpLet ev_binds, result) }
558 -- The ev_binds returned by checkConstraints is very
559 -- often empty, in which case mkWpLet is a no-op
560
561 checkConstraints :: SkolemInfo
562 -> [TcTyVar] -- Skolems
563 -> [EvVar] -- Given
564 -> TcM result
565 -> TcM (TcEvBinds, result)
566
567 checkConstraints skol_info skol_tvs given thing_inside
568 | null skol_tvs && null given
569 = do { res <- thing_inside; return (emptyTcEvBinds, res) }
570 -- Just for efficiency. We check every function argument with
571 -- tcPolyExpr, which uses tcGen and hence checkConstraints.
572
573 | otherwise
574 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
575 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
576 do { (result, tclvl, wanted) <- pushLevelAndCaptureConstraints thing_inside
577
578 ; if isEmptyWC wanted && null given
579 -- Optimisation : if there are no wanteds, and no givens
580 -- don't generate an implication at all.
581 -- Reason for the (null given): we don't want to lose
582 -- the "inaccessible alternative" error check
583 then
584 return (emptyTcEvBinds, result)
585 else do
586 { ev_binds_var <- newTcEvBinds
587 ; env <- getLclEnv
588 ; emitImplication $ Implic { ic_tclvl = tclvl
589 , ic_skols = skol_tvs
590 , ic_no_eqs = False
591 , ic_given = given
592 , ic_wanted = wanted
593 , ic_status = IC_Unsolved
594 , ic_binds = ev_binds_var
595 , ic_env = env
596 , ic_info = skol_info }
597
598 ; return (TcEvBinds ev_binds_var, result) } }
599
600 {-
601 ************************************************************************
602 * *
603 Boxy unification
604 * *
605 ************************************************************************
606
607 The exported functions are all defined as versions of some
608 non-exported generic functions.
609 -}
610
611 unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
612 -- Actual and expected types
613 -- Returns a coercion : ty1 ~ ty2
614 unifyType ty1 ty2 = uType origin ty1 ty2
615 where
616 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
617
618 ---------------
619 unifyPred :: PredType -> PredType -> TcM TcCoercion
620 -- Actual and expected types
621 unifyPred = unifyType
622
623 ---------------
624 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
625 -- Actual and expected types
626 unifyTheta theta1 theta2
627 = do { checkTc (equalLength theta1 theta2)
628 (vcat [ptext (sLit "Contexts differ in length"),
629 nest 2 $ parens $ ptext (sLit "Use RelaxedPolyRec to allow this")])
630 ; zipWithM unifyPred theta1 theta2 }
631
632 {-
633 @unifyTypeList@ takes a single list of @TauType@s and unifies them
634 all together. It is used, for example, when typechecking explicit
635 lists, when all the elts should be of the same type.
636 -}
637
638 unifyTypeList :: [TcTauType] -> TcM ()
639 unifyTypeList [] = return ()
640 unifyTypeList [_] = return ()
641 unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
642 ; unifyTypeList tys }
643
644 {-
645 ************************************************************************
646 * *
647 uType and friends
648 * *
649 ************************************************************************
650
651 uType is the heart of the unifier. Each arg occurs twice, because
652 we want to report errors in terms of synomyms if possible. The first of
653 the pair is used in error messages only; it is always the same as the
654 second, except that if the first is a synonym then the second may be a
655 de-synonym'd version. This way we get better error messages.
656 -}
657
658 ------------
659 uType, uType_defer
660 :: CtOrigin
661 -> TcType -- ty1 is the *actual* type
662 -> TcType -- ty2 is the *expected* type
663 -> TcM TcCoercion
664
665 --------------
666 -- It is always safe to defer unification to the main constraint solver
667 -- See Note [Deferred unification]
668 uType_defer origin ty1 ty2
669 = do { eqv <- newEq ty1 ty2
670 ; loc <- getCtLoc origin
671 ; emitSimple $ mkNonCanonical $
672 CtWanted { ctev_evar = eqv
673 , ctev_pred = mkTcEqPred ty1 ty2
674 , ctev_loc = loc }
675
676 -- Error trace only
677 -- NB. do *not* call mkErrInfo unless tracing is on, because
678 -- it is hugely expensive (#5631)
679 ; whenDOptM Opt_D_dump_tc_trace $ do
680 { ctxt <- getErrCtxt
681 ; doc <- mkErrInfo emptyTidyEnv ctxt
682 ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
683 ppr ty2, pprCtOrigin origin, doc])
684 }
685 ; return (mkTcCoVarCo eqv) }
686
687 --------------
688 -- unify_np (short for "no push" on the origin stack) does the work
689 uType origin orig_ty1 orig_ty2
690 = do { tclvl <- getTcLevel
691 ; traceTc "u_tys " $ vcat
692 [ text "tclvl" <+> ppr tclvl
693 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
694 , pprCtOrigin origin]
695 ; co <- go orig_ty1 orig_ty2
696 ; if isTcReflCo co
697 then traceTc "u_tys yields no coercion" Outputable.empty
698 else traceTc "u_tys yields coercion:" (ppr co)
699 ; return co }
700 where
701 go :: TcType -> TcType -> TcM TcCoercion
702 -- The arguments to 'go' are always semantically identical
703 -- to orig_ty{1,2} except for looking through type synonyms
704
705 -- Variables; go for uVar
706 -- Note that we pass in *original* (before synonym expansion),
707 -- so that type variables tend to get filled in with
708 -- the most informative version of the type
709 go (TyVarTy tv1) ty2
710 = do { lookup_res <- lookupTcTyVar tv1
711 ; case lookup_res of
712 Filled ty1 -> go ty1 ty2
713 Unfilled ds1 -> uUnfilledVar origin NotSwapped tv1 ds1 ty2 }
714 go ty1 (TyVarTy tv2)
715 = do { lookup_res <- lookupTcTyVar tv2
716 ; case lookup_res of
717 Filled ty2 -> go ty1 ty2
718 Unfilled ds2 -> uUnfilledVar origin IsSwapped tv2 ds2 ty1 }
719
720 -- See Note [Expanding synonyms during unification]
721 --
722 -- Also NB that we recurse to 'go' so that we don't push a
723 -- new item on the origin stack. As a result if we have
724 -- type Foo = Int
725 -- and we try to unify Foo ~ Bool
726 -- we'll end up saying "can't match Foo with Bool"
727 -- rather than "can't match "Int with Bool". See Trac #4535.
728 go ty1 ty2
729 | Just ty1' <- tcView ty1 = go ty1' ty2
730 | Just ty2' <- tcView ty2 = go ty1 ty2'
731
732 -- Functions (or predicate functions) just check the two parts
733 go (FunTy fun1 arg1) (FunTy fun2 arg2)
734 = do { co_l <- uType origin fun1 fun2
735 ; co_r <- uType origin arg1 arg2
736 ; return $ mkTcFunCo Nominal co_l co_r }
737
738 -- Always defer if a type synonym family (type function)
739 -- is involved. (Data families behave rigidly.)
740 go ty1@(TyConApp tc1 _) ty2
741 | isTypeFamilyTyCon tc1 = uType_defer origin ty1 ty2
742 go ty1 ty2@(TyConApp tc2 _)
743 | isTypeFamilyTyCon tc2 = uType_defer origin ty1 ty2
744
745 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
746 -- See Note [Mismatched type lists and application decomposition]
747 | tc1 == tc2, length tys1 == length tys2
748 = do { cos <- zipWithM (uType origin) tys1 tys2
749 ; return $ mkTcTyConAppCo Nominal tc1 cos }
750
751 go (LitTy m) ty@(LitTy n)
752 | m == n
753 = return $ mkTcNomReflCo ty
754
755 -- See Note [Care with type applications]
756 -- Do not decompose FunTy against App;
757 -- it's often a type error, so leave it for the constraint solver
758 go (AppTy s1 t1) (AppTy s2 t2)
759 = go_app s1 t1 s2 t2
760
761 go (AppTy s1 t1) (TyConApp tc2 ts2)
762 | Just (ts2', t2') <- snocView ts2
763 = ASSERT( isDecomposableTyCon tc2 )
764 go_app s1 t1 (TyConApp tc2 ts2') t2'
765
766 go (TyConApp tc1 ts1) (AppTy s2 t2)
767 | Just (ts1', t1') <- snocView ts1
768 = ASSERT( isDecomposableTyCon tc1 )
769 go_app (TyConApp tc1 ts1') t1' s2 t2
770
771 -- Anything else fails
772 -- E.g. unifying for-all types, which is relative unusual
773 go ty1 ty2 = uType_defer origin ty1 ty2 -- failWithMisMatch origin
774
775 ------------------
776 go_app s1 t1 s2 t2
777 = do { co_s <- uType origin s1 s2 -- See Note [Unifying AppTy]
778 ; co_t <- uType origin t1 t2
779 ; return $ mkTcAppCo co_s co_t }
780
781 {-
782 Note [Care with type applications]
783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
784 Note: type applications need a bit of care!
785 They can match FunTy and TyConApp, so use splitAppTy_maybe
786 NB: we've already dealt with type variables and Notes,
787 so if one type is an App the other one jolly well better be too
788
789 Note [Unifying AppTy]
790 ~~~~~~~~~~~~~~~~~~~~~
791 Consider unifying (m Int) ~ (IO Int) where m is a unification variable
792 that is now bound to (say) (Bool ->). Then we want to report
793 "Can't unify (Bool -> Int) with (IO Int)
794 and not
795 "Can't unify ((->) Bool) with IO"
796 That is why we use the "_np" variant of uType, which does not alter the error
797 message.
798
799 Note [Mismatched type lists and application decomposition]
800 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
801 When we find two TyConApps, you might think that the argument lists
802 are guaranteed equal length. But they aren't. Consider matching
803 w (T x) ~ Foo (T x y)
804 We do match (w ~ Foo) first, but in some circumstances we simply create
805 a deferred constraint; and then go ahead and match (T x ~ T x y).
806 This came up in Trac #3950.
807
808 So either
809 (a) either we must check for identical argument kinds
810 when decomposing applications,
811
812 (b) or we must be prepared for ill-kinded unification sub-problems
813
814 Currently we adopt (b) since it seems more robust -- no need to maintain
815 a global invariant.
816
817 Note [Expanding synonyms during unification]
818 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
819 We expand synonyms during unification, but:
820 * We expand *after* the variable case so that we tend to unify
821 variables with un-expanded type synonym. This just makes it
822 more likely that the inferred types will mention type synonyms
823 understandable to the user
824
825 * We expand *before* the TyConApp case. For example, if we have
826 type Phantom a = Int
827 and are unifying
828 Phantom Int ~ Phantom Char
829 it is *wrong* to unify Int and Char.
830
831 Note [Deferred Unification]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
833 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
834 and yet its consistency is undetermined. Previously, there was no way to still
835 make it consistent. So a mismatch error was issued.
836
837 Now these unfications are deferred until constraint simplification, where type
838 family instances and given equations may (or may not) establish the consistency.
839 Deferred unifications are of the form
840 F ... ~ ...
841 or x ~ ...
842 where F is a type function and x is a type variable.
843 E.g.
844 id :: x ~ y => x -> y
845 id e = e
846
847 involves the unfication x = y. It is deferred until we bring into account the
848 context x ~ y to establish that it holds.
849
850 If available, we defer original types (rather than those where closed type
851 synonyms have already been expanded via tcCoreView). This is, as usual, to
852 improve error messages.
853
854
855 ************************************************************************
856 * *
857 uVar and friends
858 * *
859 ************************************************************************
860
861 @uVar@ is called when at least one of the types being unified is a
862 variable. It does {\em not} assume that the variable is a fixed point
863 of the substitution; rather, notice that @uVar@ (defined below) nips
864 back into @uTys@ if it turns out that the variable is already bound.
865 -}
866
867 uUnfilledVar :: CtOrigin
868 -> SwapFlag
869 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
870 -> TcTauType -- Type 2
871 -> TcM TcCoercion
872 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
873 -- It might be a skolem, or untouchable, or meta
874
875 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
876 | tv1 == tv2 -- Same type variable => no-op
877 = return (mkTcNomReflCo (mkTyVarTy tv1))
878
879 | otherwise -- Distinct type variables
880 = do { lookup2 <- lookupTcTyVar tv2
881 ; case lookup2 of
882 Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
883 Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
884 }
885
886 uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type variable
887 = case details1 of
888 MetaTv { mtv_ref = ref1 }
889 -> do { dflags <- getDynFlags
890 ; mb_ty2' <- checkTauTvUpdate dflags tv1 non_var_ty2
891 ; case mb_ty2' of
892 Just ty2' -> updateMeta tv1 ref1 ty2'
893 Nothing -> do { traceTc "Occ/kind defer"
894 (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
895 $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
896 ; defer }
897 }
898
899 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
900 where
901 defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
902 -- Occurs check or an untouchable: just defer
903 -- NB: occurs check isn't necessarily fatal:
904 -- eg tv1 occured in type family parameter
905
906 ----------------
907 uUnfilledVars :: CtOrigin
908 -> SwapFlag
909 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
910 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
911 -> TcM TcCoercion
912 -- Invarant: The type variables are distinct,
913 -- Neither is filled in yet
914
915 uUnfilledVars origin swapped tv1 details1 tv2 details2
916 = do { traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1
917 <+> text "with" <+> ppr k2)
918 ; mb_sub_kind <- unifyKindX k1 k2
919 ; case mb_sub_kind of {
920 Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
921 Just sub_kind ->
922
923 case (sub_kind, details1, details2) of
924 -- k1 < k2, so update tv2
925 (LT, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
926
927 -- k2 < k1, so update tv1
928 (GT, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
929
930 -- k1 = k2, so we are free to update either way
931 (EQ, MetaTv { mtv_info = i1, mtv_ref = ref1 },
932 MetaTv { mtv_info = i2, mtv_ref = ref2 })
933 | nicer_to_update_tv1 tv1 i1 i2 -> updateMeta tv1 ref1 ty2
934 | otherwise -> updateMeta tv2 ref2 ty1
935 (EQ, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
936 (EQ, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
937
938 -- Can't do it in-place, so defer
939 -- This happens for skolems of all sorts
940 (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
941 where
942 k1 = tyVarKind tv1
943 k2 = tyVarKind tv2
944 ty1 = mkTyVarTy tv1
945 ty2 = mkTyVarTy tv2
946
947 nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
948 nicer_to_update_tv1 _ _ SigTv = True
949 nicer_to_update_tv1 _ SigTv _ = False
950 nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1)
951 -- Try not to update SigTvs; and try to update sys-y type
952 -- variables in preference to ones gotten (say) by
953 -- instantiating a polymorphic function with a user-written
954 -- type sig
955
956 ----------------
957 checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
958 -- (checkTauTvUpdate tv ty)
959 -- We are about to update the TauTv/ReturnTv tv with ty.
960 -- Check (a) that tv doesn't occur in ty (occurs check)
961 -- (b) that kind(ty) is a sub-kind of kind(tv)
962 --
963 -- We have two possible outcomes:
964 -- (1) Return the type to update the type variable with,
965 -- [we know the update is ok]
966 -- (2) Return Nothing,
967 -- [the update might be dodgy]
968 --
969 -- Note that "Nothing" does not mean "definite error". For example
970 -- type family F a
971 -- type instance F Int = Int
972 -- consider
973 -- a ~ F a
974 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
975 -- we return Nothing, leaving it to the later constraint simplifier to
976 -- sort matters out.
977
978 checkTauTvUpdate dflags tv ty
979 | SigTv <- info
980 = ASSERT( not (isTyVarTy ty) )
981 return Nothing
982 | otherwise
983 = do { ty <- zonkTcType ty
984 ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty)
985 ; case sub_k of
986 Nothing -> return Nothing -- Kinds don't unify
987 Just LT -> return Nothing -- (tv :: *) ~ (ty :: ?)
988 -- Don't unify because that would widen tv's kind
989
990 _ | is_return_tv -- ReturnTv: a simple occurs-check is all that we need
991 -- See Note [ReturnTv] in TcType
992 -> if tv `elemVarSet` tyVarsOfType ty
993 then return Nothing
994 else return (Just ty)
995
996 _ | defer_me ty -- Quick test
997 -> -- Failed quick test so try harder
998 case occurCheckExpand dflags tv ty of
999 OC_OK ty2 | defer_me ty2 -> return Nothing
1000 | otherwise -> return (Just ty2)
1001 _ -> return Nothing
1002
1003 _ | otherwise -> return (Just ty) }
1004 where
1005 details = ASSERT2( isMetaTyVar tv, ppr tv ) tcTyVarDetails tv
1006 info = mtv_info details
1007 is_return_tv = isReturnTyVar tv
1008 impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
1009
1010 defer_me :: TcType -> Bool
1011 -- Checks for (a) occurrence of tv
1012 -- (b) type family applications
1013 -- See Note [Conservative unification check]
1014 defer_me (LitTy {}) = False
1015 defer_me (TyVarTy tv') = tv == tv'
1016 defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
1017 defer_me (FunTy arg res) = defer_me arg || defer_me res
1018 defer_me (AppTy fun arg) = defer_me fun || defer_me arg
1019 defer_me (ForAllTy _ ty) = not impredicative || defer_me ty
1020
1021 {-
1022 Note [Conservative unification check]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 When unifying (tv ~ rhs), w try to avoid creating deferred constraints
1025 only for efficiency. However, we do not unify (the defer_me check) if
1026 a) There's an occurs check (tv is in fvs(rhs))
1027 b) There's a type-function call in 'rhs'
1028
1029 If we fail defer_me we use occurCheckExpand to try to make it pass,
1030 (see Note [Type synonyms and the occur check]) and then use defer_me
1031 again to check. Example: Trac #4917)
1032 a ~ Const a b
1033 where type Const a b = a. We can solve this immediately, even when
1034 'a' is a skolem, just by expanding the synonym.
1035
1036 We always defer type-function calls, even if it's be perfectly safe to
1037 unify, eg (a ~ F [b]). Reason: this ensures that the constraint
1038 solver gets to see, and hence simplify the type-function call, which
1039 in turn might simplify the type of an inferred function. Test ghci046
1040 is a case in point.
1041
1042 More mysteriously, test T7010 gave a horrible error
1043 T7010.hs:29:21:
1044 Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
1045 Expected type: (ValueTuple Vector, ValueTuple Vector)
1046 Actual type: (ValueTuple Vector, ValueTuple Vector)
1047 because an insoluble type function constraint got mixed up with
1048 a soluble one when flattening. I never fully understood this, but
1049 deferring type-function applications made it go away :-(.
1050 T5853 also got a less-good error message with more aggressive
1051 unification of type functions.
1052
1053 Moreover the Note [Type family sharing] gives another reason, but
1054 again I'm not sure if it's really valid.
1055
1056 Note [Type synonyms and the occur check]
1057 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1058 Generally speaking we try to update a variable with type synonyms not
1059 expanded, which improves later error messages, unless looking
1060 inside a type synonym may help resolve a spurious occurs check
1061 error. Consider:
1062 type A a = ()
1063
1064 f :: (A a -> a -> ()) -> ()
1065 f = \ _ -> ()
1066
1067 x :: ()
1068 x = f (\ x p -> p x)
1069
1070 We will eventually get a constraint of the form t ~ A t. The ok function above will
1071 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1072 unified with the original type A t, we would lead the type checker into an infinite loop.
1073
1074 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1075 the ok function expands the synonym to detect opportunities for occurs check success using
1076 the underlying definition of the type synonym.
1077
1078 The same applies later on in the constraint interaction code; see TcInteract,
1079 function @occ_check_ok@.
1080
1081 Note [Type family sharing]
1082 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1083 We must avoid eagerly unifying type variables to types that contain function symbols,
1084 because this may lead to loss of sharing, and in turn, in very poor performance of the
1085 constraint simplifier. Assume that we have a wanted constraint:
1086 {
1087 m1 ~ [F m2],
1088 m2 ~ [F m3],
1089 m3 ~ [F m4],
1090 D m1,
1091 D m2,
1092 D m3
1093 }
1094 where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
1095 then, after zonking, our constraint simplifier will be faced with the following wanted
1096 constraint:
1097 {
1098 D [F [F [F m4]]],
1099 D [F [F m4]],
1100 D [F m4]
1101 }
1102 which has to be flattened by the constraint solver. In the absence of
1103 a flat-cache, this may generate a polynomially larger number of
1104 flatten skolems and the constraint sets we are working with will be
1105 polynomially larger.
1106
1107 Instead, if we defer the unifications m1 := [F m2], etc. we will only
1108 be generating three flatten skolems, which is the maximum possible
1109 sharing arising from the original constraint. That's why we used to
1110 use a local "ok" function, a variant of TcType.occurCheckExpand.
1111
1112 HOWEVER, we *do* now have a flat-cache, which effectively recovers the
1113 sharing, so there's no great harm in losing it -- and it's generally
1114 more efficient to do the unification up-front.
1115 -}
1116
1117 data LookupTyVarResult -- The result of a lookupTcTyVar call
1118 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1119 | Filled TcType
1120
1121 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1122 lookupTcTyVar tyvar
1123 | MetaTv { mtv_ref = ref } <- details
1124 = do { meta_details <- readMutVar ref
1125 ; case meta_details of
1126 Indirect ty -> return (Filled ty)
1127 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1128 -- Note [Unifying untouchables]
1129 ; if is_touchable then
1130 return (Unfilled details)
1131 else
1132 return (Unfilled vanillaSkolemTv) } }
1133 | otherwise
1134 = return (Unfilled details)
1135 where
1136 details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
1137 tcTyVarDetails tyvar
1138
1139 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
1140 updateMeta tv1 ref1 ty2
1141 = do { writeMetaTyVarRef tv1 ref1 ty2
1142 ; return (mkTcNomReflCo ty2) }
1143
1144 {-
1145 Note [Unifying untouchables]
1146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1147 We treat an untouchable type variable as if it was a skolem. That
1148 ensures it won't unify with anything. It's a slight had, because
1149 we return a made-up TcTyVarDetails, but I think it works smoothly.
1150
1151
1152 ************************************************************************
1153 * *
1154 Kind unification
1155 * *
1156 ************************************************************************
1157
1158 Unifying kinds is much, much simpler than unifying types.
1159
1160 One small wrinkle is that as far as the user is concerned, types of kind
1161 Constraint should only be allowed to occur where we expect *exactly* that kind.
1162 We SHOULD NOT allow a type of kind fact to appear in a position expecting
1163 one of argTypeKind or openTypeKind.
1164
1165 The situation is different in the core of the compiler, where we are perfectly
1166 happy to have types of kind Constraint on either end of an arrow.
1167
1168 Note [Kind variables can be untouchable]
1169 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1170 We must use the careful function lookupTcTyVar to see if a kind
1171 variable is filled or unifiable. It checks for touchablity, and kind
1172 variables can certainly be untouchable --- for example the variable
1173 might be bound outside an enclosing existental pattern match that
1174 binds an inner kind variable, which we don't want to escape outside.
1175
1176 This, or something closely related, was the cause of Trac #8985.
1177
1178 Note [Unifying kind variables]
1179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1180 Rather hackily, kind variables can be TyVars not just TcTyVars.
1181 Main reason is in
1182 data instance T (D (x :: k)) = ...con-decls...
1183 Here we bring into scope a kind variable 'k', and use it in the
1184 con-decls. BUT the con-decls will be finished and frozen, and
1185 are not amenable to subsequent substitution, so it makes sense
1186 to have the *final* kind-variable (a KindVar, not a TcKindVar) in
1187 scope. So at least during kind unification we can encounter a
1188 KindVar.
1189
1190 Hence the isTcTyVar tests before calling lookupTcTyVar.
1191 -}
1192
1193 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1194 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1195
1196 matchExpectedFunKind (FunTy arg_kind res_kind)
1197 = return (Just (arg_kind,res_kind))
1198
1199 matchExpectedFunKind (TyVarTy kvar)
1200 | isTcTyVar kvar, isMetaTyVar kvar
1201 = do { maybe_kind <- readMetaTyVar kvar
1202 ; case maybe_kind of
1203 Indirect fun_kind -> matchExpectedFunKind fun_kind
1204 Flexi ->
1205 do { arg_kind <- newMetaKindVar
1206 ; res_kind <- newMetaKindVar
1207 ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
1208 ; return (Just (arg_kind,res_kind)) } }
1209
1210 matchExpectedFunKind _ = return Nothing
1211
1212 -----------------
1213 unifyKindX :: TcKind -- k1 (actual)
1214 -> TcKind -- k2 (expected)
1215 -> TcM (Maybe Ordering)
1216 -- Returns the relation between the kinds
1217 -- Just LT <=> k1 is a sub-kind of k2
1218 -- Nothing <=> incomparable
1219
1220 -- unifyKindX deals with the top-level sub-kinding story
1221 -- but recurses into the simpler unifyKindEq for any sub-terms
1222 -- The sub-kinding stuff only applies at top level
1223
1224 unifyKindX (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindX kv1 k2
1225 unifyKindX k1 (TyVarTy kv2) = uKVar IsSwapped unifyKindX kv2 k1
1226
1227 unifyKindX k1 k2 -- See Note [Expanding synonyms during unification]
1228 | Just k1' <- tcView k1 = unifyKindX k1' k2
1229 | Just k2' <- tcView k2 = unifyKindX k1 k2'
1230
1231 unifyKindX (TyConApp kc1 []) (TyConApp kc2 [])
1232 | kc1 == kc2 = return (Just EQ)
1233 | kc1 `tcIsSubKindCon` kc2 = return (Just LT)
1234 | kc2 `tcIsSubKindCon` kc1 = return (Just GT)
1235 | otherwise = return Nothing
1236
1237 unifyKindX k1 k2 = unifyKindEq k1 k2
1238 -- In all other cases, let unifyKindEq do the work
1239
1240 -------------------
1241 uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
1242 -> MetaKindVar -> TcKind -> TcM (Maybe Ordering)
1243 uKVar swapped unify_kind kv1 k2
1244 | isTcTyVar kv1
1245 = do { lookup_res <- lookupTcTyVar kv1 -- See Note [Kind variables can be untouchable]
1246 ; case lookup_res of
1247 Filled k1 -> unSwap swapped unify_kind k1 k2
1248 Unfilled ds1 -> uUnfilledKVar kv1 ds1 k2 }
1249
1250 | otherwise -- See Note [Unifying kind variables]
1251 = uUnfilledKVar kv1 vanillaSkolemTv k2
1252
1253 -------------------
1254 uUnfilledKVar :: MetaKindVar -> TcTyVarDetails -> TcKind -> TcM (Maybe Ordering)
1255 uUnfilledKVar kv1 ds1 (TyVarTy kv2)
1256 | kv1 == kv2
1257 = return (Just EQ)
1258
1259 | isTcTyVar kv2
1260 = do { lookup_res <- lookupTcTyVar kv2
1261 ; case lookup_res of
1262 Filled k2 -> uUnfilledKVar kv1 ds1 k2
1263 Unfilled ds2 -> uUnfilledKVars kv1 ds1 kv2 ds2 }
1264
1265 | otherwise -- See Note [Unifying kind variables]
1266 = uUnfilledKVars kv1 ds1 kv2 vanillaSkolemTv
1267
1268 uUnfilledKVar kv1 ds1 non_var_k2
1269 = case ds1 of
1270 MetaTv { mtv_info = SigTv }
1271 -> return Nothing
1272 MetaTv { mtv_ref = ref1 }
1273 -> do { k2a <- zonkTcKind non_var_k2
1274 ; let k2b = defaultKind k2a
1275 -- MetaKindVars must be bound only to simple kinds
1276
1277 ; dflags <- getDynFlags
1278 ; case occurCheckExpand dflags kv1 k2b of
1279 OC_OK k2c -> do { writeMetaTyVarRef kv1 ref1 k2c; return (Just EQ) }
1280 _ -> return Nothing }
1281 _ -> return Nothing
1282
1283 -------------------
1284 uUnfilledKVars :: MetaKindVar -> TcTyVarDetails
1285 -> MetaKindVar -> TcTyVarDetails
1286 -> TcM (Maybe Ordering)
1287 -- kv1 /= kv2
1288 uUnfilledKVars kv1 ds1 kv2 ds2
1289 = case (ds1, ds2) of
1290 (MetaTv { mtv_info = i1, mtv_ref = r1 },
1291 MetaTv { mtv_info = i2, mtv_ref = r2 })
1292 | nicer_to_update_tv1 kv1 i1 i2 -> do_update kv1 r1 kv2
1293 | otherwise -> do_update kv2 r2 kv1
1294 (MetaTv { mtv_ref = r1 }, _) -> do_update kv1 r1 kv2
1295 (_, MetaTv { mtv_ref = r2 }) -> do_update kv2 r2 kv1
1296 _ -> return Nothing
1297 where
1298 do_update kv1 r1 kv2
1299 = do { writeMetaTyVarRef kv1 r1 (mkTyVarTy kv2); return (Just EQ) }
1300
1301 ---------------------------
1302 unifyKindEq :: TcKind -> TcKind -> TcM (Maybe Ordering)
1303 -- Unify two kinds looking for equality not sub-kinding
1304 -- So it returns Nothing or (Just EQ) only
1305 unifyKindEq (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindEq kv1 k2
1306 unifyKindEq k1 (TyVarTy kv2) = uKVar IsSwapped unifyKindEq kv2 k1
1307
1308 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
1309 = do { mb1 <- unifyKindEq a1 a2; mb2 <- unifyKindEq r1 r2
1310 ; return (if isJust mb1 && isJust mb2 then Just EQ else Nothing) }
1311
1312 unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
1313 | kc1 == kc2
1314 = ASSERT(length k1s == length k2s)
1315 -- Should succeed since the kind constructors are the same,
1316 -- and the kinds are sort-checked, thus fully applied
1317 do { mb_eqs <- zipWithM unifyKindEq k1s k2s
1318 ; return (if all isJust mb_eqs
1319 then Just EQ
1320 else Nothing) }
1321
1322 unifyKindEq _ _ = return Nothing