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