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