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