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