Prevent eager unification with type families.
[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, TupleSections #-}
10
11 module TcUnify (
12 -- Full-blown subsumption
13 tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
14 tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
15 tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC,
16 checkConstraints, buildImplicationFor,
17
18 -- Various unifications
19 unifyType_, unifyType, unifyTheta, unifyKind, noThing,
20 uType, unifyExpType,
21
22 --------------------------------
23 -- Holes
24 tcInfer,
25 matchExpectedListTy,
26 matchExpectedPArrTy,
27 matchExpectedTyConApp,
28 matchExpectedAppTy,
29 matchExpectedFunTys,
30 matchActualFunTys, matchActualFunTysPart,
31 matchExpectedFunKind,
32
33 wrapFunResCoercion
34
35 ) where
36
37 #include "HsVersions.h"
38
39 import HsSyn
40 import TyCoRep
41 import TcMType
42 import TcRnMonad
43 import TcType
44 import Type
45 import Coercion
46 import TcEvidence
47 import Name ( isSystemName )
48 import Inst
49 import TyCon
50 import TysWiredIn
51 import Var
52 import VarSet
53 import VarEnv
54 import ErrUtils
55 import DynFlags
56 import BasicTypes
57 import Name ( Name )
58 import Bag
59 import Util
60 import Outputable
61 import FastString
62
63 import Control.Monad
64 import Control.Arrow ( second )
65
66 {-
67 ************************************************************************
68 * *
69 matchExpected functions
70 * *
71 ************************************************************************
72
73 Note [Herald for matchExpectedFunTys]
74 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
75 The 'herald' always looks like:
76 "The equation(s) for 'f' have"
77 "The abstraction (\x.e) takes"
78 "The section (+ x) expects"
79 "The function 'f' is applied to"
80
81 This is used to construct a message of form
82
83 The abstraction `\Just 1 -> ...' takes two arguments
84 but its type `Maybe a -> a' has only one
85
86 The equation(s) for `f' have two arguments
87 but its type `Maybe a -> a' has only one
88
89 The section `(f 3)' requires 'f' to take two arguments
90 but its type `Int -> Int' has only one
91
92 The function 'f' is applied to two arguments
93 but its type `Int -> Int' has only one
94
95 Note [matchExpectedFunTys]
96 ~~~~~~~~~~~~~~~~~~~~~~~~~~
97 matchExpectedFunTys checks that a sigma has the form
98 of an n-ary function. It passes the decomposed type to the
99 thing_inside, and returns a wrapper to coerce between the two types
100
101 It's used wherever a language construct must have a functional type,
102 namely:
103 A lambda expression
104 A function definition
105 An operator section
106
107 This function must be written CPS'd because it needs to fill in the
108 ExpTypes produced for arguments before it can fill in the ExpType
109 passed in.
110
111 -}
112
113 -- Use this one when you have an "expected" type.
114 matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
115 -> Arity
116 -> ExpRhoType -- deeply skolemised
117 -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
118 -- must fill in these ExpTypes here
119 -> TcM (a, HsWrapper)
120 -- If matchExpectedFunTys n ty = (_, wrap)
121 -- then wrap : (t1 -> ... -> tn -> ty_r) "->" ty,
122 -- where [t1, ..., tn], ty_r are passed to the thing_inside
123 matchExpectedFunTys herald arity orig_ty thing_inside
124 = case orig_ty of
125 Check ty -> go [] arity ty
126 _ -> defer [] arity orig_ty
127 where
128 go acc_arg_tys 0 ty
129 = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty)
130 ; return (result, idHsWrapper) }
131
132 go acc_arg_tys n ty
133 | Just ty' <- coreView ty = go acc_arg_tys n ty'
134
135 go acc_arg_tys n (ForAllTy (Anon arg_ty) res_ty)
136 = ASSERT( not (isPredTy arg_ty) )
137 do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
138 (n-1) res_ty
139 ; return ( result
140 , mkWpFun idHsWrapper wrap_res arg_ty res_ty ) }
141
142 go acc_arg_tys n ty@(TyVarTy tv)
143 | ASSERT( isTcTyVar tv) isMetaTyVar tv
144 = do { cts <- readMetaTyVar tv
145 ; case cts of
146 Indirect ty' -> go acc_arg_tys n ty'
147 Flexi -> defer acc_arg_tys n (mkCheckExpType ty) }
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 acc_arg_tys n ty = addErrCtxtM mk_ctxt $
165 defer acc_arg_tys n (mkCheckExpType ty)
166
167 ------------
168 defer acc_arg_tys n fun_ty
169 = do { more_arg_tys <- replicateM n newOpenInferExpType
170 ; res_ty <- newOpenInferExpType
171 ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
172 ; more_arg_tys <- mapM readExpType more_arg_tys
173 ; res_ty <- readExpType res_ty
174 ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
175 ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty
176 ; return (result, wrap) }
177
178 ------------
179 mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
180 mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_tc_ty
181 ; let (args, _) = tcSplitFunTys ty
182 n_actual = length args
183 (env'', orig_ty') = tidyOpenType env' orig_tc_ty
184 ; return ( env''
185 , mk_fun_tys_msg orig_ty' ty n_actual arity herald) }
186 where
187 orig_tc_ty = checkingExpType "matchExpectedFunTys" orig_ty
188 -- this is safe b/c we're called from "go"
189
190 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
191 -- for example in function application
192 matchActualFunTys :: Outputable a
193 => SDoc -- See Note [Herald for matchExpectedFunTys]
194 -> CtOrigin
195 -> Maybe a -- the thing with type TcSigmaType
196 -> Arity
197 -> TcSigmaType
198 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
199 -- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
200 -- then wrap : ty "->" (t1 -> ... -> tn -> ty_r)
201 matchActualFunTys herald ct_orig mb_thing arity ty
202 = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
203
204 -- | Variant of 'matchActualFunTys' that works when supplied only part
205 -- (that is, to the right of some arrows) of the full function type
206 matchActualFunTysPart :: Outputable a
207 => SDoc -- See Note [Herald for matchExpectedFunTys]
208 -> CtOrigin
209 -> Maybe a -- the thing with type TcSigmaType
210 -> Arity
211 -> TcSigmaType
212 -> [TcSigmaType] -- reversed args. See (*) below.
213 -> Arity -- overall arity of the function, for errs
214 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
215 matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
216 orig_old_args full_arity
217 = go arity orig_old_args orig_ty
218 -- Does not allocate unnecessary meta variables: if the input already is
219 -- a function, we just take it apart. Not only is this efficient,
220 -- it's important for higher rank: the argument might be of form
221 -- (forall a. ty) -> other
222 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
223 -- hide the forall inside a meta-variable
224
225 -- (*) Sometimes it's necessary to call matchActualFunTys with only part
226 -- (that is, to the right of some arrows) of the type of the function in
227 -- question. (See TcExpr.tcArgs.) This argument is the reversed list of
228 -- arguments already seen (that is, not part of the TcSigmaType passed
229 -- in elsewhere).
230
231 where
232 -- This function has a bizarre mechanic: it accumulates arguments on
233 -- the way down and also builds an argument list on the way up. Why:
234 -- 1. The returns args list and the accumulated args list might be different.
235 -- The accumulated args include all the arg types for the function,
236 -- including those from before this function was called. The returned
237 -- list should include only those arguments produced by this call of
238 -- matchActualFunTys
239 --
240 -- 2. The HsWrapper can be built only on the way up. It seems (more)
241 -- bizarre to build the HsWrapper but not the arg_tys.
242 --
243 -- Refactoring is welcome.
244 go :: Arity
245 -> [TcSigmaType] -- accumulator of arguments (reversed)
246 -> TcSigmaType -- the remainder of the type as we're processing
247 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
248 go 0 _ ty = return (idHsWrapper, [], ty)
249
250 go n acc_args ty
251 | not (null tvs && null theta)
252 = do { (wrap1, rho) <- topInstantiate ct_orig ty
253 ; (wrap2, arg_tys, res_ty) <- go n acc_args rho
254 ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
255 where
256 (tvs, theta, _) = tcSplitSigmaTy ty
257
258 go n acc_args ty
259 | Just ty' <- coreView ty = go n acc_args ty'
260
261 go n acc_args (ForAllTy (Anon arg_ty) res_ty)
262 = ASSERT( not (isPredTy arg_ty) )
263 do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
264 ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r
265 , arg_ty : tys, ty_r ) }
266
267 go n acc_args ty@(TyVarTy tv)
268 | ASSERT( isTcTyVar tv) isMetaTyVar tv
269 = do { cts <- readMetaTyVar tv
270 ; case cts of
271 Indirect ty' -> go n acc_args ty'
272 Flexi -> defer n ty }
273
274 -- In all other cases we bale out into ordinary unification
275 -- However unlike the meta-tyvar case, we are sure that the
276 -- number of arguments doesn't match arity of the original
277 -- type, so we can add a bit more context to the error message
278 -- (cf Trac #7869).
279 --
280 -- It is not always an error, because specialized type may have
281 -- different arity, for example:
282 --
283 -- > f1 = f2 'a'
284 -- > f2 :: Monad m => m Bool
285 -- > f2 = undefined
286 --
287 -- But in that case we add specialized type into error context
288 -- anyway, because it may be useful. See also Trac #9605.
289 go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
290 defer n ty
291
292 ------------
293 defer n fun_ty
294 = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
295 ; res_ty <- newOpenFlexiTyVarTy
296 ; let unif_fun_ty = mkFunTys arg_tys res_ty
297 ; co <- unifyType mb_thing fun_ty unif_fun_ty
298 ; return (mkWpCastN co, arg_tys, res_ty) }
299
300 ------------
301 mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
302 mk_ctxt arg_tys res_ty env
303 = do { let ty = mkFunTys arg_tys res_ty
304 ; (env1, zonked) <- zonkTidyTcType env ty
305 -- zonking might change # of args
306 ; let (zonked_args, _) = tcSplitFunTys zonked
307 n_actual = length zonked_args
308 (env2, unzonked) = tidyOpenType env1 ty
309 ; return ( env2
310 , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) }
311
312 mk_fun_tys_msg :: TcType -- the full type passed in (unzonked)
313 -> TcType -- the full type passed in (zonked)
314 -> Arity -- the # of args found
315 -> Arity -- the # of args wanted
316 -> SDoc -- overall herald
317 -> SDoc
318 mk_fun_tys_msg full_ty ty n_args full_arity herald
319 = herald <+> speakNOf full_arity (text "argument") <> comma $$
320 if n_args == full_arity
321 then text "its type is" <+> quotes (pprType full_ty) <>
322 comma $$
323 text "it is specialized to" <+> quotes (pprType ty)
324 else sep [text "but its type" <+> quotes (pprType ty),
325 if n_args == 0 then text "has none"
326 else text "has only" <+> speakN n_args]
327
328 ----------------------
329 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
330 -- Special case for lists
331 matchExpectedListTy exp_ty
332 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
333 ; return (co, elt_ty) }
334
335 ----------------------
336 matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
337 -- Special case for parrs
338 matchExpectedPArrTy exp_ty
339 = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
340 ; return (co, elt_ty) }
341
342 ---------------------
343 matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
344 -> TcRhoType -- orig_ty
345 -> TcM (TcCoercionN, -- T k1 k2 k3 a b c ~N orig_ty
346 [TcSigmaType]) -- Element types, k1 k2 k3 a b c
347
348 -- It's used for wired-in tycons, so we call checkWiredInTyCon
349 -- Precondition: never called with FunTyCon
350 -- Precondition: input type :: *
351 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
352
353 matchExpectedTyConApp tc orig_ty
354 = go orig_ty
355 where
356 go ty
357 | Just ty' <- coreView ty
358 = go ty'
359
360 go ty@(TyConApp tycon args)
361 | tc == tycon -- Common case
362 = return (mkTcNomReflCo ty, args)
363
364 go (TyVarTy tv)
365 | ASSERT( isTcTyVar tv) isMetaTyVar tv
366 = do { cts <- readMetaTyVar tv
367 ; case cts of
368 Indirect ty -> go ty
369 Flexi -> defer }
370
371 go _ = defer
372
373 -- If the common case does not occur, instantiate a template
374 -- T k1 .. kn t1 .. tm, and unify with the original type
375 -- Doing it this way ensures that the types we return are
376 -- kind-compatible with T. For example, suppose we have
377 -- matchExpectedTyConApp T (f Maybe)
378 -- where data T a = MkT a
379 -- Then we don't want to instantate T's data constructors with
380 -- (a::*) ~ Maybe
381 -- because that'll make types that are utterly ill-kinded.
382 -- This happened in Trac #7368
383 defer
384 = do { (_subst, args) <- tcInstBinders (tyConBinders tc)
385 ; co <- unifyType noThing (mkTyConApp tc args) orig_ty
386 ; return (co, args) }
387
388 ----------------------
389 matchExpectedAppTy :: TcRhoType -- orig_ty
390 -> TcM (TcCoercion, -- m a ~N orig_ty
391 (TcSigmaType, TcSigmaType)) -- Returns m, a
392 -- If the incoming type is a mutable type variable of kind k, then
393 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
394
395 matchExpectedAppTy orig_ty
396 = go orig_ty
397 where
398 go ty
399 | Just ty' <- coreView ty = go ty'
400
401 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
402 = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
403
404 go (TyVarTy tv)
405 | ASSERT( isTcTyVar tv) isMetaTyVar tv
406 = do { cts <- readMetaTyVar tv
407 ; case cts of
408 Indirect ty -> go ty
409 Flexi -> defer }
410
411 go _ = defer
412
413 -- Defer splitting by generating an equality constraint
414 defer
415 = do { ty1 <- newFlexiTyVarTy kind1
416 ; ty2 <- newFlexiTyVarTy kind2
417 ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
418 ; return (co, (ty1, ty2)) }
419
420 orig_kind = typeKind orig_ty
421 kind1 = mkFunTy liftedTypeKind orig_kind
422 kind2 = liftedTypeKind -- m :: * -> k
423 -- arg type :: *
424
425 {-
426 ************************************************************************
427 * *
428 Subsumption checking
429 * *
430 ************************************************************************
431
432 Note [Subsumption checking: tcSubType]
433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
434 All the tcSubType calls have the form
435 tcSubType actual_ty expected_ty
436 which checks
437 actual_ty <= expected_ty
438
439 That is, that a value of type actual_ty is acceptable in
440 a place expecting a value of type expected_ty. I.e. that
441
442 actual ty is more polymorphic than expected_ty
443
444 It returns a coercion function
445 co_fn :: actual_ty ~ expected_ty
446 which takes an HsExpr of type actual_ty into one of type
447 expected_ty.
448
449 These functions do not actually check for subsumption. They check if
450 expected_ty is an appropriate annotation to use for something of type
451 actual_ty. This difference matters when thinking about visible type
452 application. For example,
453
454 forall a. a -> forall b. b -> b
455 DOES NOT SUBSUME
456 forall a b. a -> b -> b
457
458 because the type arguments appear in a different order. (Neither does
459 it work the other way around.) BUT, these types are appropriate annotations
460 for one another. Because the user directs annotations, it's OK if some
461 arguments shuffle around -- after all, it's what the user wants.
462 Bottom line: none of this changes with visible type application.
463
464 There are a number of wrinkles (below).
465
466 Notice that Wrinkle 1 and 2 both require eta-expansion, which technically
467 may increase termination. We just put up with this, in exchange for getting
468 more predictable type inference.
469
470 Wrinkle 1: Note [Deep skolemisation]
471 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
472 We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a)
473 (see section 4.6 of "Practical type inference for higher rank types")
474 So we must deeply-skolemise the RHS before we instantiate the LHS.
475
476 That is why tc_sub_type starts with a call to tcSkolemise (which does the
477 deep skolemisation), and then calls the DS variant (which assumes
478 that expected_ty is deeply skolemised)
479
480 Wrinkle 2: Note [Co/contra-variance of subsumption checking]
481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
482 Consider g :: (Int -> Int) -> Int
483 f1 :: (forall a. a -> a) -> Int
484 f1 = g
485
486 f2 :: (forall a. a -> a) -> Int
487 f2 x = g x
488 f2 will typecheck, and it would be odd/fragile if f1 did not.
489 But f1 will only typecheck if we have that
490 (Int->Int) -> Int <= (forall a. a->a) -> Int
491 And that is only true if we do the full co/contravariant thing
492 in the subsumption check. That happens in the FunTy case of
493 tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
494 HsWrapper.
495
496 Another powerful reason for doing this co/contra stuff is visible
497 in Trac #9569, involving instantiation of constraint variables,
498 and again involving eta-expansion.
499
500 Wrinkle 3: Note [Higher rank types]
501 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
502 Consider tc150:
503 f y = \ (x::forall a. a->a). blah
504 The following happens:
505 * We will infer the type of the RHS, ie with a res_ty = alpha.
506 * Then the lambda will split alpha := beta -> gamma.
507 * And then we'll check tcSubType IsSwapped beta (forall a. a->a)
508
509 So it's important that we unify beta := forall a. a->a, rather than
510 skolemising the type.
511 -}
512
513
514 -- | Call this variant when you are in a higher-rank situation and
515 -- you know the right-hand type is deeply skolemised.
516 tcSubTypeHR :: Outputable a
517 => CtOrigin -- ^ of the actual type
518 -> Maybe a -- ^ If present, it has type ty_actual
519 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
520 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
521
522 tcSubType :: Outputable a
523 => UserTypeCtxt -> Maybe a -- ^ If present, it has type ty_actual
524 -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
525 -- Checks that actual <= expected
526 -- Returns HsWrapper :: actual ~ expected
527 tcSubType ctxt maybe_thing ty_actual ty_expected
528 = tcSubTypeO origin ctxt ty_actual ty_expected
529 where
530 origin = TypeEqOrigin { uo_actual = ty_actual
531 , uo_expected = ty_expected
532 , uo_thing = mkErrorThing <$> maybe_thing }
533
534
535 -- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
536 -- You probably want this only when looking at patterns, never expressions.
537 tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
538 tcSubTypeET orig ty_actual ty_expected
539 = uExpTypeX orig ty_expected ty_actual
540 (return . mkWpCastN . mkTcSymCo)
541 (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a
542 (mkCheckExpType ty_expected))
543
544 -- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
545 -- You probably want this only when looking at patterns, never expressions.
546 -- Does not add context.
547 tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
548 tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected
549 = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual
550 tcSubTypeET_NC ctxt (Check ty_actual) ty_expected
551 = tc_sub_type orig orig ctxt ty_actual ty_expected'
552 where
553 ty_expected' = mkCheckExpType ty_expected
554 orig = TypeEqOrigin { uo_actual = ty_actual
555 , uo_expected = ty_expected'
556 , uo_thing = Nothing }
557
558 tcSubTypeO :: CtOrigin -- ^ of the actual type
559 -> UserTypeCtxt -- ^ of the expected type
560 -> TcSigmaType
561 -> ExpSigmaType
562 -> TcM HsWrapper
563 tcSubTypeO origin ctxt ty_actual ty_expected
564 = addSubTypeCtxt ty_actual ty_expected $
565 do { traceTc "tcSubType" (vcat [ pprCtOrigin origin
566 , pprUserTypeCtxt ctxt
567 , ppr ty_actual
568 , ppr ty_expected ])
569 ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected }
570 where
571 eq_orig | TypeEqOrigin {} <- origin = origin
572 | otherwise
573 = TypeEqOrigin { uo_actual = ty_actual
574 , uo_expected = ty_expected
575 , uo_thing = Nothing }
576
577 tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a -- ^ has type ty_actual
578 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
579 -- Just like tcSubType, but with the additional precondition that
580 -- ty_expected is deeply skolemised (hence "DS")
581 tcSubTypeDS ctxt m_expr ty_actual ty_expected
582 = addSubTypeCtxt ty_actual ty_expected $
583 tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected
584
585 -- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
586 -- the "actual" type
587 tcSubTypeDS_O :: Outputable a
588 => CtOrigin -> UserTypeCtxt
589 -> Maybe a -> TcSigmaType -> ExpRhoType
590 -> TcM HsWrapper
591 tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
592 = addSubTypeCtxt ty_actual ty_expected $
593 do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
594 , pprUserTypeCtxt ctxt
595 , ppr ty_actual
596 , ppr ty_expected ])
597 ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
598
599 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
600 addSubTypeCtxt ty_actual ty_expected thing_inside
601 | isRhoTy ty_actual -- If there is no polymorphism involved, the
602 , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions)
603 = thing_inside -- gives enough context by itself
604 | otherwise
605 = addErrCtxtM mk_msg thing_inside
606 where
607 mk_msg tidy_env
608 = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual
609 -- might not be filled if we're debugging. ugh.
610 ; mb_ty_expected <- readExpType_maybe ty_expected
611 ; (tidy_env, ty_expected) <- case mb_ty_expected of
612 Just ty -> second mkCheckExpType <$>
613 zonkTidyTcType tidy_env ty
614 Nothing -> return (tidy_env, ty_expected)
615 ; ty_expected <- readExpType ty_expected
616 ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
617 ; let msg = vcat [ hang (text "When checking that:")
618 4 (ppr ty_actual)
619 , nest 2 (hang (text "is more polymorphic than:")
620 2 (ppr ty_expected)) ]
621 ; return (tidy_env, msg) }
622
623 ---------------
624 -- The "_NC" variants do not add a typechecker-error context;
625 -- the caller is assumed to do that
626
627 tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
628 tcSubType_NC ctxt ty_actual ty_expected
629 = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
630 ; tc_sub_type origin origin ctxt ty_actual ty_expected }
631 where
632 origin = TypeEqOrigin { uo_actual = ty_actual
633 , uo_expected = ty_expected
634 , uo_thing = Nothing }
635
636 tcSubTypeDS_NC :: Outputable a
637 => UserTypeCtxt
638 -> Maybe a -- ^ If present, this has type ty_actual
639 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
640 tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
641 = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
642 ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
643 where
644 origin = TypeEqOrigin { uo_actual = ty_actual
645 , uo_expected = ty_expected
646 , uo_thing = mkErrorThing <$> maybe_thing }
647
648 tcSubTypeDS_NC_O :: Outputable a
649 => CtOrigin -- origin used for instantiation only
650 -> UserTypeCtxt
651 -> Maybe a
652 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
653 -- Just like tcSubType, but with the additional precondition that
654 -- ty_expected is deeply skolemised
655 tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et
656 = uExpTypeX eq_orig ty_actual et
657 (return . mkWpCastN)
658 (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual)
659 where
660 eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et
661 , uo_thing = mkErrorThing <$> m_thing }
662
663 ---------------
664 tc_sub_type :: CtOrigin -- origin used when calling uType
665 -> CtOrigin -- origin used when instantiating
666 -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
667 tc_sub_type eq_orig inst_orig ctxt ty_actual et
668 = uExpTypeX eq_orig ty_actual et
669 (return . mkWpCastN)
670 (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual)
671
672 tc_sub_tc_type :: CtOrigin -- used when calling uType
673 -> CtOrigin -- used when instantiating
674 -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
675 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
676 | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
677 = do { lookup_res <- lookupTcTyVar tv_actual
678 ; case lookup_res of
679 Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig
680 ctxt ty_actual' ty_expected
681
682 -- It's tempting to see if tv_actual can unify with a polytype
683 -- and, if so, call uType; otherwise, skolemise first. But this
684 -- is wrong, because skolemising will bump the TcLevel and the
685 -- unification will fail anyway.
686 -- It's also tempting to call uUnfilledVar directly, but calling
687 -- uType seems safer in the presence of possible refactoring
688 -- later.
689 Unfilled _ -> mkWpCastN <$>
690 uType eq_orig TypeLevel ty_actual ty_expected }
691
692 | otherwise -- See Note [Deep skolemisation]
693 = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
694 \ _ sk_rho ->
695 tc_sub_type_ds eq_orig inst_orig ctxt
696 ty_actual sk_rho
697 ; return (sk_wrap <.> inner_wrap) }
698
699 ---------------
700 tc_sub_type_ds :: CtOrigin -- used when calling uType
701 -> CtOrigin -- used when instantiating
702 -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
703 -- Just like tcSubType, but with the additional precondition that
704 -- ty_expected is deeply skolemised
705 tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
706 = go ty_actual ty_expected
707 where
708 go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
709 | Just ty_e' <- coreView ty_e = go ty_a ty_e'
710
711 go (TyVarTy tv_a) ty_e
712 = do { lookup_res <- lookupTcTyVar tv_a
713 ; case lookup_res of
714 Filled ty_a' ->
715 do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:"
716 (ppr tv_a <+> text "-->" <+> ppr ty_a')
717 ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
718 Unfilled _ -> unify }
719
720
721 go ty_a (TyVarTy tv_e)
722 = do { dflags <- getDynFlags
723 ; tclvl <- getTcLevel
724 ; lookup_res <- lookupTcTyVar tv_e
725 ; case lookup_res of
726 Filled ty_e' ->
727 do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:"
728 (ppr tv_e <+> text "-->" <+> ppr ty_e')
729 ; tc_sub_tc_type eq_orig inst_orig ctxt ty_a ty_e' }
730 Unfilled details
731 | canUnifyWithPolyType dflags details
732 && isTouchableMetaTyVar tclvl tv_e -- don't want skolems here
733 -> unify
734
735 -- We've avoided instantiating ty_actual just in case ty_expected is
736 -- polymorphic. But we've now assiduously determined that it is *not*
737 -- polymorphic. So instantiate away. This is needed for e.g. test
738 -- typecheck/should_compile/T4284.
739 | otherwise
740 -> inst_and_unify }
741
742 go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
743 | not (isPredTy act_arg)
744 , not (isPredTy exp_arg)
745 = -- See Note [Co/contra-variance of subsumption checking]
746 do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
747 ; arg_wrap
748 <- tc_sub_tc_type eq_orig (GivenOrigin
749 (SigSkol GenSigCtxt
750 (mkCheckExpType exp_arg)))
751 ctxt exp_arg act_arg
752 ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
753 -- arg_wrap :: exp_arg ~ act_arg
754 -- res_wrap :: act-res ~ exp_res
755
756 go ty_a ty_e
757 | let (tvs, theta, _) = tcSplitSigmaTy ty_a
758 , not (null tvs && null theta)
759 = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
760 ; body_wrap <- tc_sub_type_ds
761 (eq_orig { uo_actual = in_rho
762 , uo_expected =
763 mkCheckExpType ty_expected })
764 inst_orig ctxt in_rho ty_e
765 ; return (body_wrap <.> in_wrap) }
766
767 | otherwise -- Revert to unification
768 = inst_and_unify
769 -- It's still possible that ty_actual has nested foralls. Instantiate
770 -- these, as there's no way unification will succeed with them in.
771 -- See typecheck/should_compile/T11305 for an example of when this
772 -- is important. The problem is that we're checking something like
773 -- a -> forall b. b -> b <= alpha beta gamma
774 -- where we end up with alpha := (->)
775
776 inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
777
778 -- if we haven't recurred through an arrow, then
779 -- the eq_orig will list ty_actual. In this case,
780 -- we want to update the origin to reflect the
781 -- instantiation. If we *have* recurred through
782 -- an arrow, it's better not to update.
783 ; let eq_orig' = case eq_orig of
784 TypeEqOrigin { uo_actual = orig_ty_actual }
785 | orig_ty_actual `tcEqType` ty_actual
786 , not (isIdHsWrapper wrap)
787 -> eq_orig { uo_actual = rho_a }
788 _ -> eq_orig
789
790 ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
791 ; return (mkWpCastN cow <.> wrap) }
792
793
794 -- use versions without synonyms expanded
795 unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected
796
797 -----------------
798 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
799 -- expressions
800 tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> ExpRhoType
801 -> TcM (HsExpr TcId)
802 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
803
804 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
805 -- convenient.
806 tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> ExpRhoType
807 -> TcM (HsExpr TcId)
808 tcWrapResultO orig expr actual_ty res_ty
809 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
810 , text "Expected:" <+> ppr res_ty ])
811 ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
812 (Just expr) actual_ty res_ty
813 ; return (mkHsWrap cow expr) }
814
815 -----------------------------------
816 wrapFunResCoercion
817 :: [TcType] -- Type of args
818 -> HsWrapper -- HsExpr a -> HsExpr b
819 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
820 wrapFunResCoercion arg_tys co_fn_res
821 | isIdHsWrapper co_fn_res
822 = return idHsWrapper
823 | null arg_tys
824 = return co_fn_res
825 | otherwise
826 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
827 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
828
829 -----------------------------------
830 -- | Infer a type using a fresh ExpType
831 -- See also Note [ExpType] in TcMType
832 tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType)
833 tcInfer tc_check
834 = do { res_ty <- newOpenInferExpType
835 ; result <- tc_check res_ty
836 ; res_ty <- readExpType res_ty
837 ; return (result, res_ty) }
838
839 {-
840 ************************************************************************
841 * *
842 \subsection{Generalisation}
843 * *
844 ************************************************************************
845 -}
846
847 -- | Take an "expected type" and strip off quantifiers to expose the
848 -- type underneath, binding the new skolems for the @thing_inside@.
849 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
850 tcSkolemise :: UserTypeCtxt -> TcSigmaType
851 -> ([TcTyVar] -> TcType -> TcM result)
852 -- ^ These are only ever used for scoped type variables.
853 -> TcM (HsWrapper, result)
854 -- ^ The expression has type: spec_ty -> expected_ty
855
856 tcSkolemise ctxt expected_ty thing_inside
857 -- We expect expected_ty to be a forall-type
858 -- If not, the call is a no-op
859 = do { traceTc "tcSkolemise" Outputable.empty
860 ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
861
862 ; lvl <- getTcLevel
863 ; when debugIsOn $
864 traceTc "tcSkolemise" $ vcat [
865 ppr lvl,
866 text "expected_ty" <+> ppr expected_ty,
867 text "inst tyvars" <+> ppr tvs',
868 text "given" <+> ppr given,
869 text "inst type" <+> ppr rho' ]
870
871 -- Generally we must check that the "forall_tvs" havn't been constrained
872 -- The interesting bit here is that we must include the free variables
873 -- of the expected_ty. Here's an example:
874 -- runST (newVar True)
875 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
876 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
877 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
878 -- So now s' isn't unconstrained because it's linked to a.
879 --
880 -- However [Oct 10] now that the untouchables are a range of
881 -- TcTyVars, all this is handled automatically with no need for
882 -- extra faffing around
883
884 -- Use the *instantiated* type in the SkolemInfo
885 -- so that the names of displayed type variables line up
886 ; let skol_info = SigSkol ctxt (mkCheckExpType $
887 mkFunTys (map varType given) rho')
888
889 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
890 thing_inside tvs' rho'
891
892 ; return (wrap <.> mkWpLet ev_binds, result) }
893 -- The ev_binds returned by checkConstraints is very
894 -- often empty, in which case mkWpLet is a no-op
895
896 -- | Variant of 'tcSkolemise' that takes an ExpType
897 tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
898 -> (ExpRhoType -> TcM result)
899 -> TcM (HsWrapper, result)
900 tcSkolemiseET _ et@(Infer {}) thing_inside
901 = (idHsWrapper, ) <$> thing_inside et
902 tcSkolemiseET ctxt (Check ty) thing_inside
903 = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType
904
905 checkConstraints :: SkolemInfo
906 -> [TcTyVar] -- Skolems
907 -> [EvVar] -- Given
908 -> TcM result
909 -> TcM (TcEvBinds, result)
910
911 checkConstraints skol_info skol_tvs given thing_inside
912 = do { (implics, ev_binds, result)
913 <- buildImplication skol_info skol_tvs given thing_inside
914 ; emitImplications implics
915 ; return (ev_binds, result) }
916
917 buildImplication :: SkolemInfo
918 -> [TcTyVar] -- Skolems
919 -> [EvVar] -- Given
920 -> TcM result
921 -> TcM (Bag Implication, TcEvBinds, result)
922 buildImplication skol_info skol_tvs given thing_inside
923 = do { tc_lvl <- getTcLevel
924 ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||>
925 goptM Opt_DeferTypedHoles
926 ; if null skol_tvs && null given && (not deferred_type_errors ||
927 not (isTopTcLevel tc_lvl))
928 then do { res <- thing_inside
929 ; return (emptyBag, emptyTcEvBinds, res) }
930 -- Fast path. We check every function argument with
931 -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
932 -- But with the solver producing unlifted equalities, we need
933 -- to have an EvBindsVar for them when they might be deferred to
934 -- runtime. Otherwise, they end up as top-level unlifted bindings,
935 -- which are verboten. See also Note [Deferred errors for coercion holes]
936 -- in TcErrors.
937 else
938 do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
939 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
940 ; return (implics, ev_binds, result) }}
941
942 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
943 -> [EvVar] -> WantedConstraints
944 -> TcM (Bag Implication, TcEvBinds)
945 buildImplicationFor tclvl skol_info skol_tvs given wanted
946 | isEmptyWC wanted && null given
947 -- Optimisation : if there are no wanteds, and no givens
948 -- don't generate an implication at all.
949 -- Reason for the (null given): we don't want to lose
950 -- the "inaccessible alternative" error check
951 = return (emptyBag, emptyTcEvBinds)
952
953 | otherwise
954 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
955 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
956 do { ev_binds_var <- newTcEvBinds
957 ; env <- getLclEnv
958 ; let implic = Implic { ic_tclvl = tclvl
959 , ic_skols = skol_tvs
960 , ic_no_eqs = False
961 , ic_given = given
962 , ic_wanted = wanted
963 , ic_status = IC_Unsolved
964 , ic_binds = Just ev_binds_var
965 , ic_env = env
966 , ic_info = skol_info }
967
968 ; return (unitBag implic, TcEvBinds ev_binds_var) }
969
970 {-
971 ************************************************************************
972 * *
973 Boxy unification
974 * *
975 ************************************************************************
976
977 The exported functions are all defined as versions of some
978 non-exported generic functions.
979 -}
980
981 -- | Unify two types, discarding a resultant coercion. Any constraints
982 -- generated will still need to be solved, however.
983 unifyType_ :: Outputable a => Maybe a -- ^ If present, has type 'ty1'
984 -> TcTauType -> TcTauType -> TcM ()
985 unifyType_ thing ty1 ty2 = void $ unifyType thing ty1 ty2
986
987 unifyType :: Outputable a => Maybe a -- ^ If present, has type 'ty1'
988 -> TcTauType -> TcTauType -> TcM TcCoercionN
989 -- Actual and expected types
990 -- Returns a coercion : ty1 ~ ty2
991 unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
992 where
993 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
994 , uo_thing = mkErrorThing <$> thing }
995
996 -- | Variant of 'unifyType' that takes an 'ExpType' as its second type
997 unifyExpType :: Outputable a => Maybe a
998 -> TcTauType -> ExpType -> TcM TcCoercionN
999 unifyExpType mb_thing ty1 ty2
1000 = uExpType ty_orig ty1 ty2
1001 where
1002 ty_orig = TypeEqOrigin { uo_actual = ty1
1003 , uo_expected = ty2
1004 , uo_thing = mkErrorThing <$> mb_thing }
1005
1006 -- | Use this instead of 'Nothing' when calling 'unifyType' without
1007 -- a good "thing" (where the "thing" has the "actual" type passed in)
1008 -- This has an 'Outputable' instance, avoiding amgiguity problems.
1009 noThing :: Maybe (HsExpr Name)
1010 noThing = Nothing
1011
1012 unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
1013 unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
1014 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
1015 , uo_thing = mkErrorThing <$> thing }
1016
1017 ---------------
1018 unifyPred :: PredType -> PredType -> TcM TcCoercionN
1019 -- Actual and expected types
1020 unifyPred = unifyType noThing
1021
1022 ---------------
1023 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
1024 -- Actual and expected types
1025 unifyTheta theta1 theta2
1026 = do { checkTc (equalLength theta1 theta2)
1027 (vcat [text "Contexts differ in length",
1028 nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"])
1029 ; zipWithM unifyPred theta1 theta2 }
1030
1031 {-
1032 %************************************************************************
1033 %* *
1034 uType and friends
1035 %* *
1036 %************************************************************************
1037
1038 uType is the heart of the unifier.
1039 -}
1040
1041 uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN
1042 uExpType orig ty1 et
1043 = uExpTypeX orig ty1 et return $
1044 uType orig TypeLevel ty1
1045
1046 -- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first
1047 -- continuation with the produced coercion. Otherwise, calls the second
1048 -- continuation. This can happen either with a Check or with an untouchable
1049 -- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType]
1050 uExpTypeX :: CtOrigin -> TcType -> ExpType
1051 -> (TcCoercionN -> TcM a) -- Infer case, co :: TcType ~N ExpType
1052 -> (TcType -> TcM a) -- Check / untouchable case
1053 -> TcM a
1054 uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont
1055 = do { cur_lvl <- getTcLevel
1056 ; if cur_lvl `sameDepthAs` tc_lvl
1057 then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki
1058 ; writeExpType et (ty1 `mkCastTy` ki_co)
1059 ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co }
1060 else do { traceTc "Preventing writing to untouchable ExpType" empty
1061 ; tau <- expTypeToType et -- See Note [TcLevel of ExpType]
1062 ; type_cont tau }}
1063 where
1064 kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel)
1065 uExpTypeX _ _ (Check ty2) _ type_cont
1066 = type_cont ty2
1067
1068 ------------
1069 uType, uType_defer
1070 :: CtOrigin
1071 -> TypeOrKind
1072 -> TcType -- ty1 is the *actual* type
1073 -> TcType -- ty2 is the *expected* type
1074 -> TcM Coercion
1075
1076 --------------
1077 -- It is always safe to defer unification to the main constraint solver
1078 -- See Note [Deferred unification]
1079 uType_defer origin t_or_k ty1 ty2
1080 = do { hole <- newCoercionHole
1081 ; loc <- getCtLocM origin (Just t_or_k)
1082 ; emitSimple $ mkNonCanonical $
1083 CtWanted { ctev_dest = HoleDest hole
1084 , ctev_pred = mkPrimEqPred ty1 ty2
1085 , ctev_loc = loc }
1086
1087 -- Error trace only
1088 -- NB. do *not* call mkErrInfo unless tracing is on, because
1089 -- it is hugely expensive (#5631)
1090 ; whenDOptM Opt_D_dump_tc_trace $ do
1091 { ctxt <- getErrCtxt
1092 ; doc <- mkErrInfo emptyTidyEnv ctxt
1093 ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1,
1094 ppr ty2, pprCtOrigin origin, doc])
1095 }
1096 ; return (mkHoleCo hole Nominal ty1 ty2) }
1097
1098 --------------
1099 uType origin t_or_k orig_ty1 orig_ty2
1100 = do { tclvl <- getTcLevel
1101 ; traceTc "u_tys " $ vcat
1102 [ text "tclvl" <+> ppr tclvl
1103 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
1104 , pprCtOrigin origin]
1105 ; co <- go orig_ty1 orig_ty2
1106 ; if isReflCo co
1107 then traceTc "u_tys yields no coercion" Outputable.empty
1108 else traceTc "u_tys yields coercion:" (ppr co)
1109 ; return co }
1110 where
1111 go :: TcType -> TcType -> TcM Coercion
1112 -- The arguments to 'go' are always semantically identical
1113 -- to orig_ty{1,2} except for looking through type synonyms
1114
1115 -- Variables; go for uVar
1116 -- Note that we pass in *original* (before synonym expansion),
1117 -- so that type variables tend to get filled in with
1118 -- the most informative version of the type
1119 go (TyVarTy tv1) ty2
1120 = do { lookup_res <- lookupTcTyVar tv1
1121 ; case lookup_res of
1122 Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
1123 ; go ty1 ty2 }
1124 Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 }
1125 go ty1 (TyVarTy tv2)
1126 = do { lookup_res <- lookupTcTyVar tv2
1127 ; case lookup_res of
1128 Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
1129 ; go ty1 ty2 }
1130 Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 }
1131
1132 -- See Note [Expanding synonyms during unification]
1133 go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
1134 | tc1 == tc2
1135 = return $ mkReflCo Nominal ty1
1136
1137 -- See Note [Expanding synonyms during unification]
1138 --
1139 -- Also NB that we recurse to 'go' so that we don't push a
1140 -- new item on the origin stack. As a result if we have
1141 -- type Foo = Int
1142 -- and we try to unify Foo ~ Bool
1143 -- we'll end up saying "can't match Foo with Bool"
1144 -- rather than "can't match "Int with Bool". See Trac #4535.
1145 go ty1 ty2
1146 | Just ty1' <- coreView ty1 = go ty1' ty2
1147 | Just ty2' <- coreView ty2 = go ty1 ty2'
1148
1149 go (CastTy t1 co1) t2
1150 = do { co_tys <- go t1 t2
1151 ; return (mkCoherenceLeftCo co_tys co1) }
1152
1153 go t1 (CastTy t2 co2)
1154 = do { co_tys <- go t1 t2
1155 ; return (mkCoherenceRightCo co_tys co2) }
1156
1157 -- Functions (or predicate functions) just check the two parts
1158 go (ForAllTy (Anon fun1) arg1) (ForAllTy (Anon fun2) arg2)
1159 = do { co_l <- uType origin t_or_k fun1 fun2
1160 ; co_r <- uType origin t_or_k arg1 arg2
1161 ; return $ mkFunCo Nominal co_l co_r }
1162
1163 -- Always defer if a type synonym family (type function)
1164 -- is involved. (Data families behave rigidly.)
1165 go ty1@(TyConApp tc1 _) ty2
1166 | isTypeFamilyTyCon tc1 = defer ty1 ty2
1167 go ty1 ty2@(TyConApp tc2 _)
1168 | isTypeFamilyTyCon tc2 = defer ty1 ty2
1169
1170 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1171 -- See Note [Mismatched type lists and application decomposition]
1172 | tc1 == tc2, length tys1 == length tys2
1173 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
1174 do { cos <- zipWithM (uType origin t_or_k) tys1 tys2
1175 ; return $ mkTyConAppCo Nominal tc1 cos }
1176
1177 go (LitTy m) ty@(LitTy n)
1178 | m == n
1179 = return $ mkNomReflCo ty
1180
1181 -- See Note [Care with type applications]
1182 -- Do not decompose FunTy against App;
1183 -- it's often a type error, so leave it for the constraint solver
1184 go (AppTy s1 t1) (AppTy s2 t2)
1185 = go_app s1 t1 s2 t2
1186
1187 go (AppTy s1 t1) (TyConApp tc2 ts2)
1188 | Just (ts2', t2') <- snocView ts2
1189 = ASSERT( mightBeUnsaturatedTyCon tc2 )
1190 go_app s1 t1 (TyConApp tc2 ts2') t2'
1191
1192 go (TyConApp tc1 ts1) (AppTy s2 t2)
1193 | Just (ts1', t1') <- snocView ts1
1194 = ASSERT( mightBeUnsaturatedTyCon tc1 )
1195 go_app (TyConApp tc1 ts1') t1' s2 t2
1196
1197 go (CoercionTy co1) (CoercionTy co2)
1198 = do { let ty1 = coercionType co1
1199 ty2 = coercionType co2
1200 ; kco <- uType (KindEqOrigin orig_ty1 (Just orig_ty2) origin
1201 (Just t_or_k))
1202 KindLevel
1203 ty1 ty2
1204 ; return $ mkProofIrrelCo Nominal kco co1 co2 }
1205
1206 -- Anything else fails
1207 -- E.g. unifying for-all types, which is relative unusual
1208 go ty1 ty2 = defer ty1 ty2
1209
1210 ------------------
1211 defer ty1 ty2 -- See Note [Check for equality before deferring]
1212 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
1213 | otherwise = uType_defer origin t_or_k ty1 ty2
1214
1215 ------------------
1216 go_app s1 t1 s2 t2
1217 = do { co_s <- uType origin t_or_k s1 s2
1218 ; co_t <- uType origin t_or_k t1 t2
1219 ; return $ mkAppCo co_s co_t }
1220
1221 {- Note [Check for equality before deferring]
1222 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1223 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
1224 If ty involves a type function we may defer, which isn't very sensible.
1225 An egregious example of this was in test T9872a, which has a type signature
1226 Proxy :: Proxy (Solutions Cubes)
1227 Doing the ambiguity check on this signature generates the equality
1228 Solutions Cubes ~ Solutions Cubes
1229 and currently the constraint solver normalises both sides at vast cost.
1230 This little short-cut in 'defer' helps quite a bit.
1231
1232 Note [Care with type applications]
1233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1234 Note: type applications need a bit of care!
1235 They can match FunTy and TyConApp, so use splitAppTy_maybe
1236 NB: we've already dealt with type variables and Notes,
1237 so if one type is an App the other one jolly well better be too
1238
1239 Note [Mismatched type lists and application decomposition]
1240 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1241 When we find two TyConApps, you might think that the argument lists
1242 are guaranteed equal length. But they aren't. Consider matching
1243 w (T x) ~ Foo (T x y)
1244 We do match (w ~ Foo) first, but in some circumstances we simply create
1245 a deferred constraint; and then go ahead and match (T x ~ T x y).
1246 This came up in Trac #3950.
1247
1248 So either
1249 (a) either we must check for identical argument kinds
1250 when decomposing applications,
1251
1252 (b) or we must be prepared for ill-kinded unification sub-problems
1253
1254 Currently we adopt (b) since it seems more robust -- no need to maintain
1255 a global invariant.
1256
1257 Note [Expanding synonyms during unification]
1258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1259 We expand synonyms during unification, but:
1260 * We expand *after* the variable case so that we tend to unify
1261 variables with un-expanded type synonym. This just makes it
1262 more likely that the inferred types will mention type synonyms
1263 understandable to the user
1264
1265 * We expand *before* the TyConApp case. For example, if we have
1266 type Phantom a = Int
1267 and are unifying
1268 Phantom Int ~ Phantom Char
1269 it is *wrong* to unify Int and Char.
1270
1271 * The problem case immediately above can happen only with arguments
1272 to the tycon. So we check for nullary tycons *before* expanding.
1273 This is particularly helpful when checking (* ~ *), because * is
1274 now a type synonym.
1275
1276 Note [Deferred Unification]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
1279 and yet its consistency is undetermined. Previously, there was no way to still
1280 make it consistent. So a mismatch error was issued.
1281
1282 Now these unifications are deferred until constraint simplification, where type
1283 family instances and given equations may (or may not) establish the consistency.
1284 Deferred unifications are of the form
1285 F ... ~ ...
1286 or x ~ ...
1287 where F is a type function and x is a type variable.
1288 E.g.
1289 id :: x ~ y => x -> y
1290 id e = e
1291
1292 involves the unification x = y. It is deferred until we bring into account the
1293 context x ~ y to establish that it holds.
1294
1295 If available, we defer original types (rather than those where closed type
1296 synonyms have already been expanded via tcCoreView). This is, as usual, to
1297 improve error messages.
1298
1299
1300 ************************************************************************
1301 * *
1302 uVar and friends
1303 * *
1304 ************************************************************************
1305
1306 @uVar@ is called when at least one of the types being unified is a
1307 variable. It does {\em not} assume that the variable is a fixed point
1308 of the substitution; rather, notice that @uVar@ (defined below) nips
1309 back into @uTys@ if it turns out that the variable is already bound.
1310 -}
1311
1312 uUnfilledVar :: CtOrigin
1313 -> TypeOrKind
1314 -> SwapFlag
1315 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1316 -> TcTauType -- Type 2
1317 -> TcM Coercion
1318 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
1319 -- It might be a skolem, or untouchable, or meta
1320
1321 uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2)
1322 | tv1 == tv2 -- Same type variable => no-op
1323 = return (mkNomReflCo (mkTyVarTy tv1))
1324
1325 | otherwise -- Distinct type variables
1326 = do { lookup2 <- lookupTcTyVar tv2
1327 ; case lookup2 of
1328 Filled ty2'
1329 -> uUnfilledVar origin t_or_k swapped tv1 details1 ty2'
1330 Unfilled details2
1331 -> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
1332 }
1333
1334 uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2
1335 -- ty2 is not a type variable
1336 = case details1 of
1337 MetaTv { mtv_ref = ref1 }
1338 -> do { dflags <- getDynFlags
1339 ; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2
1340 ; case mb_ty2' of
1341 Just (ty2', co_k) -> maybe_sym swapped <$>
1342 updateMeta tv1 ref1 ty2' co_k
1343 Nothing -> do { traceTc "Occ/type-family defer"
1344 (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
1345 $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
1346 ; defer }
1347 }
1348
1349 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
1350 where
1351 defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2
1352 -- Occurs check or an untouchable: just defer
1353 -- NB: occurs check isn't necessarily fatal:
1354 -- eg tv1 occured in type family parameter
1355
1356 ----------------
1357 uUnfilledVars :: CtOrigin
1358 -> TypeOrKind
1359 -> SwapFlag
1360 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1361 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
1362 -> TcM Coercion
1363 -- Invarant: The type variables are distinct,
1364 -- Neither is filled in yet
1365
1366 uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
1367 = do { traceTc "uUnfilledVars for" (ppr tv1 <+> text "and" <+> ppr tv2)
1368 ; traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1
1369 <+> text "with" <+> ppr k2)
1370 ; co_k <- uType kind_origin KindLevel k1 k2
1371 ; let no_swap ref = maybe_sym swapped <$>
1372 updateMeta tv1 ref ty2 (mkSymCo co_k)
1373 do_swap ref = maybe_sym (flipSwap swapped) <$>
1374 updateMeta tv2 ref ty1 co_k
1375 ; case (details1, details2) of
1376 { ( MetaTv { mtv_info = i1, mtv_ref = ref1 }
1377 , MetaTv { mtv_info = i2, mtv_ref = ref2 } )
1378 | nicer_to_update_tv1 tv1 i1 i2 -> no_swap ref1
1379 | otherwise -> do_swap ref2
1380 ; (MetaTv { mtv_ref = ref1 }, _) -> no_swap ref1
1381 ; (_, MetaTv { mtv_ref = ref2 }) -> do_swap ref2
1382
1383 -- Can't do it in-place, so defer
1384 -- This happens for skolems of all sorts
1385 ; _ -> do { traceTc "deferring because I can't find a meta-tyvar:"
1386 (pprTcTyVarDetails details1 <+> pprTcTyVarDetails details2)
1387 ; unSwap swapped (uType_defer origin t_or_k) ty1 ty2 } } }
1388 where
1389 k1 = tyVarKind tv1
1390 k2 = tyVarKind tv2
1391 ty1 = mkTyVarTy tv1
1392 ty2 = mkTyVarTy tv2
1393 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
1394
1395 -- | apply sym iff swapped
1396 maybe_sym :: SwapFlag -> Coercion -> Coercion
1397 maybe_sym IsSwapped = mkSymCo
1398 maybe_sym NotSwapped = id
1399
1400 nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
1401 nicer_to_update_tv1 _ _ SigTv = True
1402 nicer_to_update_tv1 _ SigTv _ = False
1403 -- Try not to update SigTvs; and try to update sys-y type
1404 -- variables in preference to ones gotten (say) by
1405 -- instantiating a polymorphic function with a user-written
1406 -- type sig
1407 nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1)
1408
1409 ----------------
1410 checkTauTvUpdate :: DynFlags
1411 -> CtOrigin
1412 -> TypeOrKind
1413 -> TcTyVar -- tv :: k1
1414 -> TcType -- ty :: k2
1415 -> TcM (Maybe ( TcType -- possibly-expanded ty
1416 , Coercion )) -- :: k2 ~N k1
1417 -- (checkTauTvUpdate tv ty)
1418 -- We are about to update the TauTv tv with ty.
1419 -- Check (a) that tv doesn't occur in ty (occurs check)
1420 -- (b) that kind(ty) matches kind(tv)
1421 --
1422 -- We have two possible outcomes:
1423 -- (1) Return the type to update the type variable with,
1424 -- [we know the update is ok]
1425 -- (2) Return Nothing,
1426 -- [the update might be dodgy]
1427 --
1428 -- Note that "Nothing" does not mean "definite error". For example
1429 -- type family F a
1430 -- type instance F Int = Int
1431 -- consider
1432 -- a ~ F a
1433 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
1434 -- we return Nothing, leaving it to the later constraint simplifier to
1435 -- sort matters out.
1436
1437 checkTauTvUpdate dflags origin t_or_k tv ty
1438 | SigTv <- info
1439 = ASSERT( not (isTyVarTy ty) )
1440 return Nothing
1441 | otherwise
1442 = do { ty <- zonkTcType ty
1443 ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
1444 ; if | defer_me ty -> -- Quick test
1445 -- Failed quick test so try harder
1446 case occurCheckExpand dflags tv ty of
1447 OC_OK ty2 | defer_me ty2 -> return Nothing
1448 | otherwise -> return (Just (ty2, co_k))
1449 _ -> return Nothing
1450 | otherwise -> return (Just (ty, co_k)) }
1451
1452 where
1453 kind_origin = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
1454 details = tcTyVarDetails tv
1455 info = mtv_info details
1456
1457 impredicative = canUnifyWithPolyType dflags details
1458
1459 defer_me :: TcType -> Bool
1460 -- Checks for (a) occurrence of tv
1461 -- (b) type family applications
1462 -- (c) foralls
1463 -- See Note [Prevent unification with type families]
1464 -- See Note [Refactoring hazard: checkTauTvUpdate]
1465 defer_me (LitTy {}) = False
1466 defer_me (TyVarTy tv') = tv == tv' || defer_me (tyVarKind tv')
1467 defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
1468 || not (impredicative || isTauTyCon tc)
1469 defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t
1470 || (isNamedBinder bndr && not impredicative)
1471 defer_me (AppTy fun arg) = defer_me fun || defer_me arg
1472 defer_me (CastTy ty co) = defer_me ty || defer_me_co co
1473 defer_me (CoercionTy co) = defer_me_co co
1474
1475 -- We don't really care if there are type families in a coercion,
1476 -- but we still can't have an occurs-check failure
1477 defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
1478
1479 {-
1480 Note [Prevent unification with type families]
1481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1482 We prevent unification with type families because of an uneasy compromise.
1483 It's perfectly sound to unify with type families, and it even improves the
1484 error messages in the testsuite. It also modestly improves performance, at
1485 least in some cases. But it's disastrous for test case perf/compiler/T3064.
1486 Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
1487 What do we do? Do we reduce F? Or do we use the given? Hard to know what's
1488 best. GHC reduces. This is a disaster for T3064, where the type's size
1489 spirals out of control during reduction. (We're not helped by the fact that
1490 the flattener re-flattens all the arguments every time around.) If we prevent
1491 unification with type families, then the solver happens to use the equality
1492 before expanding the type family.
1493
1494 It would be lovely in the future to revisit this problem and remove this
1495 extra, unnecessary check. But we retain it for now as it seems to work
1496 better in practice.
1497
1498 Note [Refactoring hazard: checkTauTvUpdate]
1499 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1500 I (Richard E.) have a sad story about refactoring this code, retained here
1501 to prevent others (or a future me!) from falling into the same traps.
1502
1503 It all started with #11407, which was caused by the fact that the TyVarTy
1504 case of defer_me didn't look in the kind. But it seemed reasonable to
1505 simply remove the defer_me check instead.
1506
1507 It referred to two Notes (since removed) that were out of date, and the
1508 fast_check code in occurCheckExpand seemed to do just about the same thing as
1509 defer_me. The one piece that defer_me did that wasn't repeated by
1510 occurCheckExpand was the type-family check. (See Note [Prevent unification
1511 with type families].) So I checked the result of occurCheckExpand for any
1512 type family occurrences and deferred if there were any. This was done
1513 in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
1514
1515 This approach turned out not to be performant, because the expanded type
1516 was bigger than the original type, and tyConsOfType looks through type
1517 synonyms. So it then struck me that we could dispense with the defer_me
1518 check entirely. This simplified the code nicely, and it cut the allocations
1519 in T5030 by half. But, as documented in Note [Prevent unification with
1520 type families], this destroyed performance in T3064. Regardless, I missed this
1521 regression and the change was committed as
1522 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
1523
1524 Bottom lines:
1525 * defer_me is back, but now fixed w.r.t. #11407.
1526 * Tread carefully before you start to refactor here. There can be
1527 lots of hard-to-predict consequences.
1528
1529 Note [Type synonyms and the occur check]
1530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1531 Generally speaking we try to update a variable with type synonyms not
1532 expanded, which improves later error messages, unless looking
1533 inside a type synonym may help resolve a spurious occurs check
1534 error. Consider:
1535 type A a = ()
1536
1537 f :: (A a -> a -> ()) -> ()
1538 f = \ _ -> ()
1539
1540 x :: ()
1541 x = f (\ x p -> p x)
1542
1543 We will eventually get a constraint of the form t ~ A t. The ok function above will
1544 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1545 unified with the original type A t, we would lead the type checker into an infinite loop.
1546
1547 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1548 the ok function expands the synonym to detect opportunities for occurs check success using
1549 the underlying definition of the type synonym.
1550
1551 The same applies later on in the constraint interaction code; see TcInteract,
1552 function @occ_check_ok@.
1553
1554 Note [Non-TcTyVars in TcUnify]
1555 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1556 Because the same code is now shared between unifying types and unifying
1557 kinds, we sometimes will see proper TyVars floating around the unifier.
1558 Example (from test case polykinds/PolyKinds12):
1559
1560 type family Apply (f :: k1 -> k2) (x :: k1) :: k2
1561 type instance Apply g y = g y
1562
1563 When checking the instance declaration, we first *kind-check* the LHS
1564 and RHS, discovering that the instance really should be
1565
1566 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
1567
1568 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
1569 as a second pass, we desugar the RHS (which is done in functions prefixed
1570 with "tc" in TcTyClsDecls"). By this time, all the kind-vars are proper
1571 TyVars, not TcTyVars, get some kind unification must happen.
1572
1573 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
1574 meta-tyvar.
1575
1576 This used to not be necessary for type-checking (that is, before * :: *)
1577 because expressions get desugared via an algorithm separate from
1578 type-checking (with wrappers, etc.). Types get desugared very differently,
1579 causing this wibble in behavior seen here.
1580 -}
1581
1582 data LookupTyVarResult -- The result of a lookupTcTyVar call
1583 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1584 | Filled TcType
1585
1586 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1587 lookupTcTyVar tyvar
1588 | MetaTv { mtv_ref = ref } <- details
1589 = do { meta_details <- readMutVar ref
1590 ; case meta_details of
1591 Indirect ty -> return (Filled ty)
1592 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1593 -- Note [Unifying untouchables]
1594 ; if is_touchable then
1595 return (Unfilled details)
1596 else
1597 return (Unfilled vanillaSkolemTv) } }
1598 | otherwise
1599 = return (Unfilled details)
1600 where
1601 details = tcTyVarDetails tyvar
1602
1603 -- | Fill in a meta-tyvar
1604 updateMeta :: TcTyVar -- ^ tv to fill in, tv :: k1
1605 -> TcRef MetaDetails -- ^ ref to tv's metadetails
1606 -> TcType -- ^ ty2 :: k2
1607 -> Coercion -- ^ kind_co :: k2 ~N k1
1608 -> TcM Coercion -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
1609 updateMeta tv1 ref1 ty2 kind_co
1610 = do { let ty2_refl = mkNomReflCo ty2
1611 (ty2', co) = ( ty2 `mkCastTy` kind_co
1612 , mkCoherenceLeftCo ty2_refl kind_co )
1613 ; writeMetaTyVarRef tv1 ref1 ty2'
1614 ; return co }
1615
1616 {-
1617 Note [Unifying untouchables]
1618 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1619 We treat an untouchable type variable as if it was a skolem. That
1620 ensures it won't unify with anything. It's a slight had, because
1621 we return a made-up TcTyVarDetails, but I think it works smoothly.
1622 -}
1623
1624 -- | Breaks apart a function kind into its pieces.
1625 matchExpectedFunKind :: Arity -- ^ # of args remaining, only for errors
1626 -> TcType -- ^ type, only for errors
1627 -> TcKind -- ^ function kind
1628 -> TcM (Coercion, TcKind, TcKind)
1629 -- ^ co :: old_kind ~ arg -> res
1630 matchExpectedFunKind num_args_remaining ty = go
1631 where
1632 go k | Just k' <- coreView k = go k'
1633
1634 go k@(TyVarTy kvar)
1635 | isTcTyVar kvar, isMetaTyVar kvar
1636 = do { maybe_kind <- readMetaTyVar kvar
1637 ; case maybe_kind of
1638 Indirect fun_kind -> go fun_kind
1639 Flexi -> defer k }
1640
1641 go k@(ForAllTy (Anon arg) res)
1642 = return (mkNomReflCo k, arg, res)
1643
1644 go other = defer other
1645
1646 defer k
1647 = do { arg_kind <- newMetaKindVar
1648 ; res_kind <- newMetaKindVar
1649 ; let new_fun = mkFunTy arg_kind res_kind
1650 thing = mkTypeErrorThingArgs ty num_args_remaining
1651 origin = TypeEqOrigin { uo_actual = k
1652 , uo_expected = mkCheckExpType new_fun
1653 , uo_thing = Just thing
1654 }
1655 ; co <- uType origin KindLevel k new_fun
1656 ; return (co, arg_kind, res_kind) }
1657 where