Major patch to add -fwarn-redundant-constraints
[ghc.git] / compiler / typecheck / TcUnify.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Type subsumption and unification
7 -}
8
9 {-# LANGUAGE CPP #-}
10
11 module TcUnify (
12 -- Full-blown subsumption
13 tcWrapResult, tcGen,
14 tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
15 checkConstraints,
16
17 -- Various unifications
18 unifyType, unifyTypeList, unifyTheta,
19 unifyKindX,
20
21 --------------------------------
22 -- Holes
23 tcInfer,
24 matchExpectedListTy,
25 matchExpectedPArrTy,
26 matchExpectedTyConApp,
27 matchExpectedAppTy,
28 matchExpectedFunTys,
29 matchExpectedFunKind,
30 wrapFunResCoercion
31
32 ) where
33
34 #include "HsVersions.h"
35
36 import HsSyn
37 import TypeRep
38 import TcMType
39 import TcRnMonad
40 import TcType
41 import Type
42 import TcEvidence
43 import Name ( isSystemName )
44 import Inst
45 import Kind
46 import TyCon
47 import TysWiredIn
48 import Var
49 import VarEnv
50 import VarSet
51 import ErrUtils
52 import DynFlags
53 import BasicTypes
54 import Maybes ( isJust )
55 import Util
56 import Outputable
57 import FastString
58
59 import Control.Monad
60
61 {-
62 ************************************************************************
63 * *
64 matchExpected functions
65 * *
66 ************************************************************************
67
68 Note [Herald for matchExpectedFunTys]
69 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
70 The 'herald' always looks like:
71 "The equation(s) for 'f' have"
72 "The abstraction (\x.e) takes"
73 "The section (+ x) expects"
74 "The function 'f' is applied to"
75
76 This is used to construct a message of form
77
78 The abstraction `\Just 1 -> ...' takes two arguments
79 but its type `Maybe a -> a' has only one
80
81 The equation(s) for `f' have two arguments
82 but its type `Maybe a -> a' has only one
83
84 The section `(f 3)' requires 'f' to take two arguments
85 but its type `Int -> Int' has only one
86
87 The function 'f' is applied to two arguments
88 but its type `Int -> Int' has only one
89
90 Note [matchExpectedFunTys]
91 ~~~~~~~~~~~~~~~~~~~~~~~~~~
92 matchExpectedFunTys checks that an (Expected rho) has the form
93 of an n-ary function. It passes the decomposed type to the
94 thing_inside, and returns a wrapper to coerce between the two types
95
96 It's used wherever a language construct must have a functional type,
97 namely:
98 A lambda expression
99 A function definition
100 An operator section
101
102 This is not (currently) where deep skolemisation occurs;
103 matchExpectedFunTys does not skolmise nested foralls in the
104 expected type, because it expects that to have been done already
105 -}
106
107 matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
108 -> Arity
109 -> TcRhoType
110 -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
111
112 -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
113 -- then co : ty ~ (t1 -> ... -> tn -> ty_r)
114 --
115 -- Does not allocate unnecessary meta variables: if the input already is
116 -- a function, we just take it apart. Not only is this efficient,
117 -- it's important for higher rank: the argument might be of form
118 -- (forall a. ty) -> other
119 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
120 -- hide the forall inside a meta-variable
121
122 matchExpectedFunTys herald arity orig_ty
123 = go arity orig_ty
124 where
125 -- If go n ty = (co, [t1,..,tn], ty_r)
126 -- then co : ty ~ t1 -> .. -> tn -> ty_r
127
128 go n_req ty
129 | n_req == 0 = return (mkTcNomReflCo ty, [], ty)
130
131 go n_req ty
132 | Just ty' <- tcView ty = go n_req ty'
133
134 go n_req (FunTy arg_ty res_ty)
135 | not (isPredTy arg_ty)
136 = do { (co, tys, ty_r) <- go (n_req-1) res_ty
137 ; return (mkTcFunCo Nominal (mkTcNomReflCo arg_ty) co, arg_ty:tys, ty_r) }
138
139 go n_req ty@(TyVarTy tv)
140 | ASSERT( isTcTyVar tv) isMetaTyVar tv
141 = do { cts <- readMetaTyVar tv
142 ; case cts of
143 Indirect ty' -> go n_req ty'
144 Flexi -> defer n_req ty }
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 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
569 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
570 do { (result, tclvl, wanted) <- pushLevelAndCaptureConstraints thing_inside
571
572 ; if isEmptyWC wanted && null given
573 -- Optimisation : if there are no wanteds, and no givens
574 -- don't generate an implication at all.
575 -- Reason for the (null given): we don't want to lose
576 -- the "inaccessible alternative" error check
577 then
578 return (emptyTcEvBinds, result)
579 else do
580 { ev_binds_var <- newTcEvBinds
581 ; env <- getLclEnv
582 ; emitImplication $ Implic { ic_tclvl = tclvl
583 , ic_skols = skol_tvs
584 , ic_no_eqs = False
585 , ic_given = given
586 , ic_wanted = wanted
587 , ic_status = IC_Unsolved
588 , ic_binds = ev_binds_var
589 , ic_env = env
590 , ic_info = skol_info }
591
592 ; return (TcEvBinds ev_binds_var, result) } }
593
594 {-
595 ************************************************************************
596 * *
597 Boxy unification
598 * *
599 ************************************************************************
600
601 The exported functions are all defined as versions of some
602 non-exported generic functions.
603 -}
604
605 unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
606 -- Actual and expected types
607 -- Returns a coercion : ty1 ~ ty2
608 unifyType ty1 ty2 = uType origin ty1 ty2
609 where
610 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
611
612 ---------------
613 unifyPred :: PredType -> PredType -> TcM TcCoercion
614 -- Actual and expected types
615 unifyPred = unifyType
616
617 ---------------
618 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
619 -- Actual and expected types
620 unifyTheta theta1 theta2
621 = do { checkTc (equalLength theta1 theta2)
622 (vcat [ptext (sLit "Contexts differ in length"),
623 nest 2 $ parens $ ptext (sLit "Use RelaxedPolyRec to allow this")])
624 ; zipWithM unifyPred theta1 theta2 }
625
626 {-
627 @unifyTypeList@ takes a single list of @TauType@s and unifies them
628 all together. It is used, for example, when typechecking explicit
629 lists, when all the elts should be of the same type.
630 -}
631
632 unifyTypeList :: [TcTauType] -> TcM ()
633 unifyTypeList [] = return ()
634 unifyTypeList [_] = return ()
635 unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
636 ; unifyTypeList tys }
637
638 {-
639 ************************************************************************
640 * *
641 uType and friends
642 * *
643 ************************************************************************
644
645 uType is the heart of the unifier. Each arg occurs twice, because
646 we want to report errors in terms of synomyms if possible. The first of
647 the pair is used in error messages only; it is always the same as the
648 second, except that if the first is a synonym then the second may be a
649 de-synonym'd version. This way we get better error messages.
650 -}
651
652 ------------
653 uType, uType_defer
654 :: CtOrigin
655 -> TcType -- ty1 is the *actual* type
656 -> TcType -- ty2 is the *expected* type
657 -> TcM TcCoercion
658
659 --------------
660 -- It is always safe to defer unification to the main constraint solver
661 -- See Note [Deferred unification]
662 uType_defer origin ty1 ty2
663 = do { eqv <- newEq ty1 ty2
664 ; loc <- getCtLoc origin
665 ; emitSimple $ mkNonCanonical $
666 CtWanted { ctev_evar = eqv
667 , ctev_pred = mkTcEqPred ty1 ty2
668 , ctev_loc = loc }
669
670 -- Error trace only
671 -- NB. do *not* call mkErrInfo unless tracing is on, because
672 -- it is hugely expensive (#5631)
673 ; whenDOptM Opt_D_dump_tc_trace $ do
674 { ctxt <- getErrCtxt
675 ; doc <- mkErrInfo emptyTidyEnv ctxt
676 ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
677 ppr ty2, pprCtOrigin origin, doc])
678 }
679 ; return (mkTcCoVarCo eqv) }
680
681 --------------
682 -- unify_np (short for "no push" on the origin stack) does the work
683 uType origin orig_ty1 orig_ty2
684 = do { tclvl <- getTcLevel
685 ; traceTc "u_tys " $ vcat
686 [ text "tclvl" <+> ppr tclvl
687 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
688 , pprCtOrigin origin]
689 ; co <- go orig_ty1 orig_ty2
690 ; if isTcReflCo co
691 then traceTc "u_tys yields no coercion" Outputable.empty
692 else traceTc "u_tys yields coercion:" (ppr co)
693 ; return co }
694 where
695 go :: TcType -> TcType -> TcM TcCoercion
696 -- The arguments to 'go' are always semantically identical
697 -- to orig_ty{1,2} except for looking through type synonyms
698
699 -- Variables; go for uVar
700 -- Note that we pass in *original* (before synonym expansion),
701 -- so that type variables tend to get filled in with
702 -- the most informative version of the type
703 go (TyVarTy tv1) ty2
704 = do { lookup_res <- lookupTcTyVar tv1
705 ; case lookup_res of
706 Filled ty1 -> go ty1 ty2
707 Unfilled ds1 -> uUnfilledVar origin NotSwapped tv1 ds1 ty2 }
708 go ty1 (TyVarTy tv2)
709 = do { lookup_res <- lookupTcTyVar tv2
710 ; case lookup_res of
711 Filled ty2 -> go ty1 ty2
712 Unfilled ds2 -> uUnfilledVar origin IsSwapped tv2 ds2 ty1 }
713
714 -- See Note [Expanding synonyms during unification]
715 --
716 -- Also NB that we recurse to 'go' so that we don't push a
717 -- new item on the origin stack. As a result if we have
718 -- type Foo = Int
719 -- and we try to unify Foo ~ Bool
720 -- we'll end up saying "can't match Foo with Bool"
721 -- rather than "can't match "Int with Bool". See Trac #4535.
722 go ty1 ty2
723 | Just ty1' <- tcView ty1 = go ty1' ty2
724 | Just ty2' <- tcView ty2 = go ty1 ty2'
725
726 -- Functions (or predicate functions) just check the two parts
727 go (FunTy fun1 arg1) (FunTy fun2 arg2)
728 = do { co_l <- uType origin fun1 fun2
729 ; co_r <- uType origin arg1 arg2
730 ; return $ mkTcFunCo Nominal co_l co_r }
731
732 -- Always defer if a type synonym family (type function)
733 -- is involved. (Data families behave rigidly.)
734 go ty1@(TyConApp tc1 _) ty2
735 | isTypeFamilyTyCon tc1 = uType_defer origin ty1 ty2
736 go ty1 ty2@(TyConApp tc2 _)
737 | isTypeFamilyTyCon tc2 = uType_defer origin ty1 ty2
738
739 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
740 -- See Note [Mismatched type lists and application decomposition]
741 | tc1 == tc2, length tys1 == length tys2
742 = do { cos <- zipWithM (uType origin) tys1 tys2
743 ; return $ mkTcTyConAppCo Nominal tc1 cos }
744
745 go (LitTy m) ty@(LitTy n)
746 | m == n
747 = return $ mkTcNomReflCo ty
748
749 -- See Note [Care with type applications]
750 -- Do not decompose FunTy against App;
751 -- it's often a type error, so leave it for the constraint solver
752 go (AppTy s1 t1) (AppTy s2 t2)
753 = go_app s1 t1 s2 t2
754
755 go (AppTy s1 t1) (TyConApp tc2 ts2)
756 | Just (ts2', t2') <- snocView ts2
757 = ASSERT( isDecomposableTyCon tc2 )
758 go_app s1 t1 (TyConApp tc2 ts2') t2'
759
760 go (TyConApp tc1 ts1) (AppTy s2 t2)
761 | Just (ts1', t1') <- snocView ts1
762 = ASSERT( isDecomposableTyCon tc1 )
763 go_app (TyConApp tc1 ts1') t1' s2 t2
764
765 -- Anything else fails
766 -- E.g. unifying for-all types, which is relative unusual
767 go ty1 ty2 = uType_defer origin ty1 ty2 -- failWithMisMatch origin
768
769 ------------------
770 go_app s1 t1 s2 t2
771 = do { co_s <- uType origin s1 s2 -- See Note [Unifying AppTy]
772 ; co_t <- uType origin t1 t2
773 ; return $ mkTcAppCo co_s co_t }
774
775 {-
776 Note [Care with type applications]
777 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
778 Note: type applications need a bit of care!
779 They can match FunTy and TyConApp, so use splitAppTy_maybe
780 NB: we've already dealt with type variables and Notes,
781 so if one type is an App the other one jolly well better be too
782
783 Note [Unifying AppTy]
784 ~~~~~~~~~~~~~~~~~~~~~
785 Consider unifying (m Int) ~ (IO Int) where m is a unification variable
786 that is now bound to (say) (Bool ->). Then we want to report
787 "Can't unify (Bool -> Int) with (IO Int)
788 and not
789 "Can't unify ((->) Bool) with IO"
790 That is why we use the "_np" variant of uType, which does not alter the error
791 message.
792
793 Note [Mismatched type lists and application decomposition]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 When we find two TyConApps, you might think that the argument lists
796 are guaranteed equal length. But they aren't. Consider matching
797 w (T x) ~ Foo (T x y)
798 We do match (w ~ Foo) first, but in some circumstances we simply create
799 a deferred constraint; and then go ahead and match (T x ~ T x y).
800 This came up in Trac #3950.
801
802 So either
803 (a) either we must check for identical argument kinds
804 when decomposing applications,
805
806 (b) or we must be prepared for ill-kinded unification sub-problems
807
808 Currently we adopt (b) since it seems more robust -- no need to maintain
809 a global invariant.
810
811 Note [Expanding synonyms during unification]
812 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
813 We expand synonyms during unification, but:
814 * We expand *after* the variable case so that we tend to unify
815 variables with un-expanded type synonym. This just makes it
816 more likely that the inferred types will mention type synonyms
817 understandable to the user
818
819 * We expand *before* the TyConApp case. For example, if we have
820 type Phantom a = Int
821 and are unifying
822 Phantom Int ~ Phantom Char
823 it is *wrong* to unify Int and Char.
824
825 Note [Deferred Unification]
826 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
827 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
828 and yet its consistency is undetermined. Previously, there was no way to still
829 make it consistent. So a mismatch error was issued.
830
831 Now these unfications are deferred until constraint simplification, where type
832 family instances and given equations may (or may not) establish the consistency.
833 Deferred unifications are of the form
834 F ... ~ ...
835 or x ~ ...
836 where F is a type function and x is a type variable.
837 E.g.
838 id :: x ~ y => x -> y
839 id e = e
840
841 involves the unfication x = y. It is deferred until we bring into account the
842 context x ~ y to establish that it holds.
843
844 If available, we defer original types (rather than those where closed type
845 synonyms have already been expanded via tcCoreView). This is, as usual, to
846 improve error messages.
847
848
849 ************************************************************************
850 * *
851 uVar and friends
852 * *
853 ************************************************************************
854
855 @uVar@ is called when at least one of the types being unified is a
856 variable. It does {\em not} assume that the variable is a fixed point
857 of the substitution; rather, notice that @uVar@ (defined below) nips
858 back into @uTys@ if it turns out that the variable is already bound.
859 -}
860
861 uUnfilledVar :: CtOrigin
862 -> SwapFlag
863 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
864 -> TcTauType -- Type 2
865 -> TcM TcCoercion
866 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
867 -- It might be a skolem, or untouchable, or meta
868
869 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
870 | tv1 == tv2 -- Same type variable => no-op
871 = return (mkTcNomReflCo (mkTyVarTy tv1))
872
873 | otherwise -- Distinct type variables
874 = do { lookup2 <- lookupTcTyVar tv2
875 ; case lookup2 of
876 Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
877 Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
878 }
879
880 uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type variable
881 = case details1 of
882 MetaTv { mtv_ref = ref1 }
883 -> do { dflags <- getDynFlags
884 ; mb_ty2' <- checkTauTvUpdate dflags tv1 non_var_ty2
885 ; case mb_ty2' of
886 Just ty2' -> updateMeta tv1 ref1 ty2'
887 Nothing -> do { traceTc "Occ/kind defer"
888 (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
889 $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
890 ; defer }
891 }
892
893 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
894 where
895 defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
896 -- Occurs check or an untouchable: just defer
897 -- NB: occurs check isn't necessarily fatal:
898 -- eg tv1 occured in type family parameter
899
900 ----------------
901 uUnfilledVars :: CtOrigin
902 -> SwapFlag
903 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
904 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
905 -> TcM TcCoercion
906 -- Invarant: The type variables are distinct,
907 -- Neither is filled in yet
908
909 uUnfilledVars origin swapped tv1 details1 tv2 details2
910 = do { traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1
911 <+> text "with" <+> ppr k2)
912 ; mb_sub_kind <- unifyKindX k1 k2
913 ; case mb_sub_kind of {
914 Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
915 Just sub_kind ->
916
917 case (sub_kind, details1, details2) of
918 -- k1 < k2, so update tv2
919 (LT, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
920
921 -- k2 < k1, so update tv1
922 (GT, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
923
924 -- k1 = k2, so we are free to update either way
925 (EQ, MetaTv { mtv_info = i1, mtv_ref = ref1 },
926 MetaTv { mtv_info = i2, mtv_ref = ref2 })
927 | nicer_to_update_tv1 tv1 i1 i2 -> updateMeta tv1 ref1 ty2
928 | otherwise -> updateMeta tv2 ref2 ty1
929 (EQ, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
930 (EQ, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
931
932 -- Can't do it in-place, so defer
933 -- This happens for skolems of all sorts
934 (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
935 where
936 k1 = tyVarKind tv1
937 k2 = tyVarKind tv2
938 ty1 = mkTyVarTy tv1
939 ty2 = mkTyVarTy tv2
940
941 nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
942 nicer_to_update_tv1 _ _ SigTv = True
943 nicer_to_update_tv1 _ SigTv _ = False
944 nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1)
945 -- Try not to update SigTvs; and try to update sys-y type
946 -- variables in preference to ones gotten (say) by
947 -- instantiating a polymorphic function with a user-written
948 -- type sig
949
950 ----------------
951 checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
952 -- (checkTauTvUpdate tv ty)
953 -- We are about to update the TauTv/ReturnTv tv with ty.
954 -- Check (a) that tv doesn't occur in ty (occurs check)
955 -- (b) that kind(ty) is a sub-kind of kind(tv)
956 --
957 -- We have two possible outcomes:
958 -- (1) Return the type to update the type variable with,
959 -- [we know the update is ok]
960 -- (2) Return Nothing,
961 -- [the update might be dodgy]
962 --
963 -- Note that "Nothing" does not mean "definite error". For example
964 -- type family F a
965 -- type instance F Int = Int
966 -- consider
967 -- a ~ F a
968 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
969 -- we return Nothing, leaving it to the later constraint simplifier to
970 -- sort matters out.
971
972 checkTauTvUpdate dflags tv ty
973 | SigTv <- info
974 = ASSERT( not (isTyVarTy ty) )
975 return Nothing
976 | otherwise
977 = do { ty1 <- zonkTcType ty
978 ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1)
979 ; case sub_k of
980 Nothing -> return Nothing
981 Just LT -> return Nothing
982 _ | is_return_tv -> if tv `elemVarSet` tyVarsOfType ty
983 then return Nothing
984 else return (Just ty1)
985 _ | defer_me ty1 -- Quick test
986 -> -- Failed quick test so try harder
987 case occurCheckExpand dflags tv ty1 of
988 OC_OK ty2 | defer_me ty2 -> return Nothing
989 | otherwise -> return (Just ty2)
990 _ -> return Nothing
991 | otherwise -> return (Just ty1) }
992 where
993 details = ASSERT2( isMetaTyVar tv, ppr tv ) tcTyVarDetails tv
994 info = mtv_info details
995 is_return_tv = case info of { ReturnTv -> True; _ -> False }
996 impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
997
998 defer_me :: TcType -> Bool
999 -- Checks for (a) occurrence of tv
1000 -- (b) type family applications
1001 -- See Note [Conservative unification check]
1002 defer_me (LitTy {}) = False
1003 defer_me (TyVarTy tv') = tv == tv'
1004 defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
1005 defer_me (FunTy arg res) = defer_me arg || defer_me res
1006 defer_me (AppTy fun arg) = defer_me fun || defer_me arg
1007 defer_me (ForAllTy _ ty) = not impredicative || defer_me ty
1008
1009 {-
1010 Note [Conservative unification check]
1011 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1012 When unifying (tv ~ rhs), w try to avoid creating deferred constraints
1013 only for efficiency. However, we do not unify (the defer_me check) if
1014 a) There's an occurs check (tv is in fvs(rhs))
1015 b) There's a type-function call in 'rhs'
1016
1017 If we fail defer_me we use occurCheckExpand to try to make it pass,
1018 (see Note [Type synonyms and the occur check]) and then use defer_me
1019 again to check. Example: Trac #4917)
1020 a ~ Const a b
1021 where type Const a b = a. We can solve this immediately, even when
1022 'a' is a skolem, just by expanding the synonym.
1023
1024 We always defer type-function calls, even if it's be perfectly safe to
1025 unify, eg (a ~ F [b]). Reason: this ensures that the constraint
1026 solver gets to see, and hence simplify the type-function call, which
1027 in turn might simplify the type of an inferred function. Test ghci046
1028 is a case in point.
1029
1030 More mysteriously, test T7010 gave a horrible error
1031 T7010.hs:29:21:
1032 Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
1033 Expected type: (ValueTuple Vector, ValueTuple Vector)
1034 Actual type: (ValueTuple Vector, ValueTuple Vector)
1035 because an insoluble type function constraint got mixed up with
1036 a soluble one when flattening. I never fully understood this, but
1037 deferring type-function applications made it go away :-(.
1038 T5853 also got a less-good error message with more aggressive
1039 unification of type functions.
1040
1041 Moreover the Note [Type family sharing] gives another reason, but
1042 again I'm not sure if it's really valid.
1043
1044 Note [Type synonyms and the occur check]
1045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1046 Generally speaking we try to update a variable with type synonyms not
1047 expanded, which improves later error messages, unless looking
1048 inside a type synonym may help resolve a spurious occurs check
1049 error. Consider:
1050 type A a = ()
1051
1052 f :: (A a -> a -> ()) -> ()
1053 f = \ _ -> ()
1054
1055 x :: ()
1056 x = f (\ x p -> p x)
1057
1058 We will eventually get a constraint of the form t ~ A t. The ok function above will
1059 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1060 unified with the original type A t, we would lead the type checker into an infinite loop.
1061
1062 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1063 the ok function expands the synonym to detect opportunities for occurs check success using
1064 the underlying definition of the type synonym.
1065
1066 The same applies later on in the constraint interaction code; see TcInteract,
1067 function @occ_check_ok@.
1068
1069 Note [Type family sharing]
1070 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1071 We must avoid eagerly unifying type variables to types that contain function symbols,
1072 because this may lead to loss of sharing, and in turn, in very poor performance of the
1073 constraint simplifier. Assume that we have a wanted constraint:
1074 {
1075 m1 ~ [F m2],
1076 m2 ~ [F m3],
1077 m3 ~ [F m4],
1078 D m1,
1079 D m2,
1080 D m3
1081 }
1082 where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
1083 then, after zonking, our constraint simplifier will be faced with the following wanted
1084 constraint:
1085 {
1086 D [F [F [F m4]]],
1087 D [F [F m4]],
1088 D [F m4]
1089 }
1090 which has to be flattened by the constraint solver. In the absence of
1091 a flat-cache, this may generate a polynomially larger number of
1092 flatten skolems and the constraint sets we are working with will be
1093 polynomially larger.
1094
1095 Instead, if we defer the unifications m1 := [F m2], etc. we will only
1096 be generating three flatten skolems, which is the maximum possible
1097 sharing arising from the original constraint. That's why we used to
1098 use a local "ok" function, a variant of TcType.occurCheckExpand.
1099
1100 HOWEVER, we *do* now have a flat-cache, which effectively recovers the
1101 sharing, so there's no great harm in losing it -- and it's generally
1102 more efficient to do the unification up-front.
1103 -}
1104
1105 data LookupTyVarResult -- The result of a lookupTcTyVar call
1106 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1107 | Filled TcType
1108
1109 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1110 lookupTcTyVar tyvar
1111 | MetaTv { mtv_ref = ref } <- details
1112 = do { meta_details <- readMutVar ref
1113 ; case meta_details of
1114 Indirect ty -> return (Filled ty)
1115 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1116 -- Note [Unifying untouchables]
1117 ; if is_touchable then
1118 return (Unfilled details)
1119 else
1120 return (Unfilled vanillaSkolemTv) } }
1121 | otherwise
1122 = return (Unfilled details)
1123 where
1124 details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
1125 tcTyVarDetails tyvar
1126
1127 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
1128 updateMeta tv1 ref1 ty2
1129 = do { writeMetaTyVarRef tv1 ref1 ty2
1130 ; return (mkTcNomReflCo ty2) }
1131
1132 {-
1133 Note [Unifying untouchables]
1134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1135 We treat an untouchable type variable as if it was a skolem. That
1136 ensures it won't unify with anything. It's a slight had, because
1137 we return a made-up TcTyVarDetails, but I think it works smoothly.
1138
1139
1140 ************************************************************************
1141 * *
1142 Kind unification
1143 * *
1144 ************************************************************************
1145
1146 Unifying kinds is much, much simpler than unifying types.
1147
1148 One small wrinkle is that as far as the user is concerned, types of kind
1149 Constraint should only be allowed to occur where we expect *exactly* that kind.
1150 We SHOULD NOT allow a type of kind fact to appear in a position expecting
1151 one of argTypeKind or openTypeKind.
1152
1153 The situation is different in the core of the compiler, where we are perfectly
1154 happy to have types of kind Constraint on either end of an arrow.
1155
1156 Note [Kind variables can be untouchable]
1157 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1158 We must use the careful function lookupTcTyVar to see if a kind
1159 variable is filled or unifiable. It checks for touchablity, and kind
1160 variables can certainly be untouchable --- for example the variable
1161 might be bound outside an enclosing existental pattern match that
1162 binds an inner kind variable, which we don't want to escape outside.
1163
1164 This, or something closely related, was the cause of Trac #8985.
1165
1166 Note [Unifying kind variables]
1167 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1168 Rather hackily, kind variables can be TyVars not just TcTyVars.
1169 Main reason is in
1170 data instance T (D (x :: k)) = ...con-decls...
1171 Here we bring into scope a kind variable 'k', and use it in the
1172 con-decls. BUT the con-decls will be finished and frozen, and
1173 are not amenable to subsequent substitution, so it makes sense
1174 to have the *final* kind-variable (a KindVar, not a TcKindVar) in
1175 scope. So at least during kind unification we can encounter a
1176 KindVar.
1177
1178 Hence the isTcTyVar tests before calling lookupTcTyVar.
1179 -}
1180
1181 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1182 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1183
1184 matchExpectedFunKind (FunTy arg_kind res_kind)
1185 = return (Just (arg_kind,res_kind))
1186
1187 matchExpectedFunKind (TyVarTy kvar)
1188 | isTcTyVar kvar, isMetaTyVar kvar
1189 = do { maybe_kind <- readMetaTyVar kvar
1190 ; case maybe_kind of
1191 Indirect fun_kind -> matchExpectedFunKind fun_kind
1192 Flexi ->
1193 do { arg_kind <- newMetaKindVar
1194 ; res_kind <- newMetaKindVar
1195 ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
1196 ; return (Just (arg_kind,res_kind)) } }
1197
1198 matchExpectedFunKind _ = return Nothing
1199
1200 -----------------
1201 unifyKindX :: TcKind -- k1 (actual)
1202 -> TcKind -- k2 (expected)
1203 -> TcM (Maybe Ordering)
1204 -- Returns the relation between the kinds
1205 -- Just LT <=> k1 is a sub-kind of k2
1206 -- Nothing <=> incomparable
1207
1208 -- unifyKindX deals with the top-level sub-kinding story
1209 -- but recurses into the simpler unifyKindEq for any sub-terms
1210 -- The sub-kinding stuff only applies at top level
1211
1212 unifyKindX (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindX kv1 k2
1213 unifyKindX k1 (TyVarTy kv2) = uKVar IsSwapped unifyKindX kv2 k1
1214
1215 unifyKindX k1 k2 -- See Note [Expanding synonyms during unification]
1216 | Just k1' <- tcView k1 = unifyKindX k1' k2
1217 | Just k2' <- tcView k2 = unifyKindX k1 k2'
1218
1219 unifyKindX (TyConApp kc1 []) (TyConApp kc2 [])
1220 | kc1 == kc2 = return (Just EQ)
1221 | kc1 `tcIsSubKindCon` kc2 = return (Just LT)
1222 | kc2 `tcIsSubKindCon` kc1 = return (Just GT)
1223 | otherwise = return Nothing
1224
1225 unifyKindX k1 k2 = unifyKindEq k1 k2
1226 -- In all other cases, let unifyKindEq do the work
1227
1228 -------------------
1229 uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
1230 -> MetaKindVar -> TcKind -> TcM (Maybe Ordering)
1231 uKVar swapped unify_kind kv1 k2
1232 | isTcTyVar kv1
1233 = do { lookup_res <- lookupTcTyVar kv1 -- See Note [Kind variables can be untouchable]
1234 ; case lookup_res of
1235 Filled k1 -> unSwap swapped unify_kind k1 k2
1236 Unfilled ds1 -> uUnfilledKVar kv1 ds1 k2 }
1237
1238 | otherwise -- See Note [Unifying kind variables]
1239 = uUnfilledKVar kv1 vanillaSkolemTv k2
1240
1241 -------------------
1242 uUnfilledKVar :: MetaKindVar -> TcTyVarDetails -> TcKind -> TcM (Maybe Ordering)
1243 uUnfilledKVar kv1 ds1 (TyVarTy kv2)
1244 | kv1 == kv2
1245 = return (Just EQ)
1246
1247 | isTcTyVar kv2
1248 = do { lookup_res <- lookupTcTyVar kv2
1249 ; case lookup_res of
1250 Filled k2 -> uUnfilledKVar kv1 ds1 k2
1251 Unfilled ds2 -> uUnfilledKVars kv1 ds1 kv2 ds2 }
1252
1253 | otherwise -- See Note [Unifying kind variables]
1254 = uUnfilledKVars kv1 ds1 kv2 vanillaSkolemTv
1255
1256 uUnfilledKVar kv1 ds1 non_var_k2
1257 = case ds1 of
1258 MetaTv { mtv_info = SigTv }
1259 -> return Nothing
1260 MetaTv { mtv_ref = ref1 }
1261 -> do { k2a <- zonkTcKind non_var_k2
1262 ; let k2b = defaultKind k2a
1263 -- MetaKindVars must be bound only to simple kinds
1264
1265 ; dflags <- getDynFlags
1266 ; case occurCheckExpand dflags kv1 k2b of
1267 OC_OK k2c -> do { writeMetaTyVarRef kv1 ref1 k2c; return (Just EQ) }
1268 _ -> return Nothing }
1269 _ -> return Nothing
1270
1271 -------------------
1272 uUnfilledKVars :: MetaKindVar -> TcTyVarDetails
1273 -> MetaKindVar -> TcTyVarDetails
1274 -> TcM (Maybe Ordering)
1275 -- kv1 /= kv2
1276 uUnfilledKVars kv1 ds1 kv2 ds2
1277 = case (ds1, ds2) of
1278 (MetaTv { mtv_info = i1, mtv_ref = r1 },
1279 MetaTv { mtv_info = i2, mtv_ref = r2 })
1280 | nicer_to_update_tv1 kv1 i1 i2 -> do_update kv1 r1 kv2
1281 | otherwise -> do_update kv2 r2 kv1
1282 (MetaTv { mtv_ref = r1 }, _) -> do_update kv1 r1 kv2
1283 (_, MetaTv { mtv_ref = r2 }) -> do_update kv2 r2 kv1
1284 _ -> return Nothing
1285 where
1286 do_update kv1 r1 kv2
1287 = do { writeMetaTyVarRef kv1 r1 (mkTyVarTy kv2); return (Just EQ) }
1288
1289 ---------------------------
1290 unifyKindEq :: TcKind -> TcKind -> TcM (Maybe Ordering)
1291 -- Unify two kinds looking for equality not sub-kinding
1292 -- So it returns Nothing or (Just EQ) only
1293 unifyKindEq (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindEq kv1 k2
1294 unifyKindEq k1 (TyVarTy kv2) = uKVar IsSwapped unifyKindEq kv2 k1
1295
1296 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
1297 = do { mb1 <- unifyKindEq a1 a2; mb2 <- unifyKindEq r1 r2
1298 ; return (if isJust mb1 && isJust mb2 then Just EQ else Nothing) }
1299
1300 unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
1301 | kc1 == kc2
1302 = ASSERT(length k1s == length k2s)
1303 -- Should succeed since the kind constructors are the same,
1304 -- and the kinds are sort-checked, thus fully applied
1305 do { mb_eqs <- zipWithM unifyKindEq k1s k2s
1306 ; return (if all isJust mb_eqs
1307 then Just EQ
1308 else Nothing) }
1309
1310 unifyKindEq _ _ = return Nothing