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