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