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