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