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