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