Visible type application
[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 _ -> mkWpCastN <$> 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 -> mkWpCastN <$> 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 -> do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
656
657 -- if we haven't recurred through an arrow, then
658 -- the eq_orig will list ty_actual. In this case,
659 -- we want to update the origin to reflect the
660 -- instantiation. If we *have* recurred through
661 -- an arrow, it's better not to update.
662 ; let eq_orig' = case eq_orig of
663 TypeEqOrigin { uo_actual = orig_ty_actual
664 , uo_expected = orig_ty_expected
665 , uo_thing = thing }
666 | orig_ty_actual `tcEqType` ty_actual
667 -> TypeEqOrigin
668 { uo_actual = rho_a
669 , uo_expected = orig_ty_expected
670 , uo_thing = thing }
671 _ -> eq_orig
672
673 ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
674 ; return (mkWpCastN cow <.> wrap) } }
675
676 go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
677 | not (isPredTy act_arg)
678 , not (isPredTy exp_arg)
679 = -- See Note [Co/contra-variance of subsumption checking]
680 do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
681 ; arg_wrap
682 <- tc_sub_type eq_orig (GivenOrigin (SigSkol GenSigCtxt exp_arg))
683 ctxt exp_arg act_arg
684 ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
685 -- arg_wrap :: exp_arg ~ act_arg
686 -- res_wrap :: act-res ~ exp_res
687
688 go ty_a ty_e
689 | let (tvs, theta, _) = tcSplitSigmaTy ty_a
690 , not (null tvs && null theta)
691 = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
692 ; body_wrap <- tcSubTypeDS_NC_O inst_orig ctxt noThing in_rho ty_e
693 ; return (body_wrap <.> in_wrap) }
694
695 | otherwise -- Revert to unification
696 = do { cow <- unify
697 ; return (mkWpCastN cow) }
698
699 -- use versions without synonyms expanded
700 unify = uType eq_orig TypeLevel ty_actual ty_expected
701
702 -----------------
703 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
704 -- expressions
705 tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> TcRhoType
706 -> TcM (HsExpr TcId)
707 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
708
709 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
710 -- convenient.
711 tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> TcRhoType
712 -> TcM (HsExpr TcId)
713 tcWrapResultO orig expr actual_ty res_ty
714 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
715 , text "Expected:" <+> ppr res_ty ])
716 ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
717 (Just expr) actual_ty res_ty
718 ; return (mkHsWrap cow expr) }
719
720 -----------------------------------
721 wrapFunResCoercion
722 :: [TcType] -- Type of args
723 -> HsWrapper -- HsExpr a -> HsExpr b
724 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
725 wrapFunResCoercion arg_tys co_fn_res
726 | isIdHsWrapper co_fn_res
727 = return idHsWrapper
728 | null arg_tys
729 = return co_fn_res
730 | otherwise
731 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
732 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
733
734 -----------------------------------
735 -- | Infer a type using a type "checking" function by passing in a ReturnTv,
736 -- which can unify with *anything*. See also Note [ReturnTv] in TcType
737 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
738 tcInfer tc_check
739 = do { (ret_tv, ret_kind) <- newOpenReturnTyVar
740 ; res <- tc_check (mkTyVarTy ret_tv)
741 ; details <- readMetaTyVar ret_tv
742 ; res_ty <- case details of
743 Indirect ty -> return ty
744 Flexi -> -- Checking was uninformative
745 do { traceTc "Defaulting un-filled ReturnTv to a TauTv" (ppr ret_tv)
746 ; tau_ty <- newFlexiTyVarTy ret_kind
747 ; writeMetaTyVar ret_tv tau_ty
748 ; return tau_ty }
749 ; return (res, res_ty) }
750
751 {-
752 ************************************************************************
753 * *
754 \subsection{Generalisation}
755 * *
756 ************************************************************************
757 -}
758
759 -- | Take an "expected type" and strip off quantifiers to expose the
760 -- type underneath, binding the new skolems for the @thing_inside@.
761 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
762 tcSkolemise :: UserTypeCtxt -> TcSigmaType
763 -> ([TcTyVar] -> TcType -> TcM result)
764 -- ^ thing_inside is passed only the *type* variables, not
765 -- *coercion* variables. They are only ever used for scoped type
766 -- variables.
767 -> TcM (HsWrapper, result)
768 -- ^ The expression has type: spec_ty -> expected_ty
769
770 tcSkolemise ctxt expected_ty thing_inside
771 -- We expect expected_ty to be a forall-type
772 -- If not, the call is a no-op
773 = do { traceTc "tcSkolemise" Outputable.empty
774 ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
775
776 ; lvl <- getTcLevel
777 ; when debugIsOn $
778 traceTc "tcSkolemise" $ vcat [
779 ppr lvl,
780 text "expected_ty" <+> ppr expected_ty,
781 text "inst tyvars" <+> ppr tvs',
782 text "given" <+> ppr given,
783 text "inst type" <+> ppr rho' ]
784
785 -- Generally we must check that the "forall_tvs" havn't been constrained
786 -- The interesting bit here is that we must include the free variables
787 -- of the expected_ty. Here's an example:
788 -- runST (newVar True)
789 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
790 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
791 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
792 -- So now s' isn't unconstrained because it's linked to a.
793 --
794 -- However [Oct 10] now that the untouchables are a range of
795 -- TcTyVars, all this is handled automatically with no need for
796 -- extra faffing around
797
798 -- Use the *instantiated* type in the SkolemInfo
799 -- so that the names of displayed type variables line up
800 ; let skol_info = SigSkol ctxt (mkFunTys (map varType given) rho')
801
802 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
803 thing_inside tvs' rho'
804
805 ; return (wrap <.> mkWpLet ev_binds, result) }
806 -- The ev_binds returned by checkConstraints is very
807 -- often empty, in which case mkWpLet is a no-op
808
809 checkConstraints :: SkolemInfo
810 -> [TcTyVar] -- Skolems
811 -> [EvVar] -- Given
812 -> TcM result
813 -> TcM (TcEvBinds, result)
814
815 checkConstraints skol_info skol_tvs given thing_inside
816 = do { (implics, ev_binds, result)
817 <- buildImplication skol_info skol_tvs given thing_inside
818 ; emitImplications implics
819 ; return (ev_binds, result) }
820
821 buildImplication :: SkolemInfo
822 -> [TcTyVar] -- Skolems
823 -> [EvVar] -- Given
824 -> TcM result
825 -> TcM (Bag Implication, TcEvBinds, result)
826 buildImplication skol_info skol_tvs given thing_inside
827 = do { tc_lvl <- getTcLevel
828 ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||>
829 goptM Opt_DeferTypedHoles
830 ; if null skol_tvs && null given && (not deferred_type_errors ||
831 not (isTopTcLevel tc_lvl))
832 then do { res <- thing_inside
833 ; return (emptyBag, emptyTcEvBinds, res) }
834 -- Fast path. We check every function argument with
835 -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
836 -- But with the solver producing unlifted equalities, we need
837 -- to have an EvBindsVar for them when they might be deferred to
838 -- runtime. Otherwise, they end up as top-level unlifted bindings,
839 -- which are verboten. See also Note [Deferred errors for coercion holes]
840 -- in TcErrors.
841 else
842 do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
843 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
844 ; return (implics, ev_binds, result) }}
845
846 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
847 -> [EvVar] -> WantedConstraints
848 -> TcM (Bag Implication, TcEvBinds)
849 buildImplicationFor tclvl skol_info skol_tvs given wanted
850 | isEmptyWC wanted && null given
851 -- Optimisation : if there are no wanteds, and no givens
852 -- don't generate an implication at all.
853 -- Reason for the (null given): we don't want to lose
854 -- the "inaccessible alternative" error check
855 = return (emptyBag, emptyTcEvBinds)
856
857 | otherwise
858 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
859 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
860 do { ev_binds_var <- newTcEvBinds
861 ; env <- getLclEnv
862 ; let implic = Implic { ic_tclvl = tclvl
863 , ic_skols = skol_tvs
864 , ic_no_eqs = False
865 , ic_given = given
866 , ic_wanted = wanted
867 , ic_status = IC_Unsolved
868 , ic_binds = Just ev_binds_var
869 , ic_env = env
870 , ic_info = skol_info }
871
872 ; return (unitBag implic, TcEvBinds ev_binds_var) }
873
874 {-
875 ************************************************************************
876 * *
877 Boxy unification
878 * *
879 ************************************************************************
880
881 The exported functions are all defined as versions of some
882 non-exported generic functions.
883 -}
884
885 -- | Unify two types, discarding a resultant coercion. Any constraints
886 -- generated will still need to be solved, however.
887 unifyType_ :: Outputable a => Maybe a -- ^ If present, has type 'ty1'
888 -> TcTauType -> TcTauType -> TcM ()
889 unifyType_ thing ty1 ty2 = void $ unifyType thing ty1 ty2
890
891 unifyType :: Outputable a => Maybe a -- ^ If present, has type 'ty1'
892 -> TcTauType -> TcTauType -> TcM TcCoercion
893 -- Actual and expected types
894 -- Returns a coercion : ty1 ~ ty2
895 unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
896 where
897 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
898 , uo_thing = mkErrorThing <$> thing }
899
900 -- | Use this instead of 'Nothing' when calling 'unifyType' without
901 -- a good "thing" (where the "thing" has the "actual" type passed in)
902 -- This has an 'Outputable' instance, avoiding amgiguity problems.
903 noThing :: Maybe (HsExpr Name)
904 noThing = Nothing
905
906 unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM Coercion
907 unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
908 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
909 , uo_thing = mkErrorThing <$> thing }
910
911 ---------------
912 unifyPred :: PredType -> PredType -> TcM TcCoercion
913 -- Actual and expected types
914 unifyPred = unifyType noThing
915
916 ---------------
917 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
918 -- Actual and expected types
919 unifyTheta theta1 theta2
920 = do { checkTc (equalLength theta1 theta2)
921 (vcat [ptext (sLit "Contexts differ in length"),
922 nest 2 $ parens $ ptext (sLit "Use RelaxedPolyRec to allow this")])
923 ; zipWithM unifyPred theta1 theta2 }
924
925 {-
926 %************************************************************************
927 %* *
928 uType and friends
929 %* *
930 %************************************************************************
931
932 uType is the heart of the unifier.
933 -}
934
935 ------------
936 uType, uType_defer
937 :: CtOrigin
938 -> TypeOrKind
939 -> TcType -- ty1 is the *actual* type
940 -> TcType -- ty2 is the *expected* type
941 -> TcM Coercion
942
943 --------------
944 -- It is always safe to defer unification to the main constraint solver
945 -- See Note [Deferred unification]
946 uType_defer origin t_or_k ty1 ty2
947 = do { hole <- newCoercionHole
948 ; loc <- getCtLocM origin (Just t_or_k)
949 ; emitSimple $ mkNonCanonical $
950 CtWanted { ctev_dest = HoleDest hole
951 , ctev_pred = mkPrimEqPred ty1 ty2
952 , ctev_loc = loc }
953
954 -- Error trace only
955 -- NB. do *not* call mkErrInfo unless tracing is on, because
956 -- it is hugely expensive (#5631)
957 ; whenDOptM Opt_D_dump_tc_trace $ do
958 { ctxt <- getErrCtxt
959 ; doc <- mkErrInfo emptyTidyEnv ctxt
960 ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1,
961 ppr ty2, pprCtOrigin origin, doc])
962 }
963 ; return (mkHoleCo hole Nominal ty1 ty2) }
964
965 --------------
966 uType origin t_or_k orig_ty1 orig_ty2
967 = do { tclvl <- getTcLevel
968 ; traceTc "u_tys " $ vcat
969 [ text "tclvl" <+> ppr tclvl
970 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
971 , pprCtOrigin origin]
972 ; co <- go orig_ty1 orig_ty2
973 ; if isReflCo co
974 then traceTc "u_tys yields no coercion" Outputable.empty
975 else traceTc "u_tys yields coercion:" (ppr co)
976 ; return co }
977 where
978 go :: TcType -> TcType -> TcM Coercion
979 -- The arguments to 'go' are always semantically identical
980 -- to orig_ty{1,2} except for looking through type synonyms
981
982 -- Variables; go for uVar
983 -- Note that we pass in *original* (before synonym expansion),
984 -- so that type variables tend to get filled in with
985 -- the most informative version of the type
986 go (TyVarTy tv1) ty2
987 = do { lookup_res <- lookupTcTyVar tv1
988 ; case lookup_res of
989 Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
990 ; go ty1 ty2 }
991 Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 }
992 go ty1 (TyVarTy tv2)
993 = do { lookup_res <- lookupTcTyVar tv2
994 ; case lookup_res of
995 Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
996 ; go ty1 ty2 }
997 Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 }
998
999 -- See Note [Expanding synonyms during unification]
1000 go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
1001 | tc1 == tc2
1002 = return $ mkReflCo Nominal ty1
1003
1004 -- See Note [Expanding synonyms during unification]
1005 --
1006 -- Also NB that we recurse to 'go' so that we don't push a
1007 -- new item on the origin stack. As a result if we have
1008 -- type Foo = Int
1009 -- and we try to unify Foo ~ Bool
1010 -- we'll end up saying "can't match Foo with Bool"
1011 -- rather than "can't match "Int with Bool". See Trac #4535.
1012 go ty1 ty2
1013 | Just ty1' <- coreView ty1 = go ty1' ty2
1014 | Just ty2' <- coreView ty2 = go ty1 ty2'
1015
1016 go (CastTy t1 co1) t2
1017 = do { co_tys <- go t1 t2
1018 ; return (mkCoherenceLeftCo co_tys co1) }
1019
1020 go t1 (CastTy t2 co2)
1021 = do { co_tys <- go t1 t2
1022 ; return (mkCoherenceRightCo co_tys co2) }
1023
1024 -- Functions (or predicate functions) just check the two parts
1025 go (ForAllTy (Anon fun1) arg1) (ForAllTy (Anon fun2) arg2)
1026 = do { co_l <- uType origin t_or_k fun1 fun2
1027 ; co_r <- uType origin t_or_k arg1 arg2
1028 ; return $ mkFunCo Nominal co_l co_r }
1029
1030 -- Always defer if a type synonym family (type function)
1031 -- is involved. (Data families behave rigidly.)
1032 go ty1@(TyConApp tc1 _) ty2
1033 | isTypeFamilyTyCon tc1 = defer ty1 ty2
1034 go ty1 ty2@(TyConApp tc2 _)
1035 | isTypeFamilyTyCon tc2 = defer ty1 ty2
1036
1037 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1038 -- See Note [Mismatched type lists and application decomposition]
1039 | tc1 == tc2, length tys1 == length tys2
1040 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
1041 do { cos <- zipWith3M (uType origin) t_or_ks tys1 tys2
1042 ; return $ mkTyConAppCo Nominal tc1 cos }
1043 where
1044 (bndrs, _) = splitPiTys (tyConKind tc1)
1045 t_or_ks = case t_or_k of
1046 KindLevel -> repeat KindLevel
1047 TypeLevel -> map (\bndr -> if isNamedBinder bndr
1048 then KindLevel
1049 else TypeLevel)
1050 bndrs
1051
1052 go (LitTy m) ty@(LitTy n)
1053 | m == n
1054 = return $ mkNomReflCo ty
1055
1056 -- See Note [Care with type applications]
1057 -- Do not decompose FunTy against App;
1058 -- it's often a type error, so leave it for the constraint solver
1059 go (AppTy s1 t1) (AppTy s2 t2)
1060 = go_app s1 t1 s2 t2
1061
1062 go (AppTy s1 t1) (TyConApp tc2 ts2)
1063 | Just (ts2', t2') <- snocView ts2
1064 = ASSERT( mightBeUnsaturatedTyCon tc2 )
1065 go_app s1 t1 (TyConApp tc2 ts2') t2'
1066
1067 go (TyConApp tc1 ts1) (AppTy s2 t2)
1068 | Just (ts1', t1') <- snocView ts1
1069 = ASSERT( mightBeUnsaturatedTyCon tc1 )
1070 go_app (TyConApp tc1 ts1') t1' s2 t2
1071
1072 go (CoercionTy co1) (CoercionTy co2)
1073 = do { let ty1 = coercionType co1
1074 ty2 = coercionType co2
1075 ; kco <- uType (KindEqOrigin orig_ty1 orig_ty2 origin (Just t_or_k))
1076 KindLevel
1077 ty1 ty2
1078 ; return $ mkProofIrrelCo Nominal kco co1 co2 }
1079
1080 -- Anything else fails
1081 -- E.g. unifying for-all types, which is relative unusual
1082 go ty1 ty2 = defer ty1 ty2
1083
1084 ------------------
1085 defer ty1 ty2 -- See Note [Check for equality before deferring]
1086 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
1087 | otherwise = uType_defer origin t_or_k ty1 ty2
1088
1089 ------------------
1090 go_app s1 t1 s2 t2
1091 = do { co_s <- uType origin t_or_k s1 s2
1092 ; co_t <- uType origin t_or_k t1 t2
1093 ; return $ mkAppCo co_s co_t }
1094
1095 {- Note [Check for equality before deferring]
1096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1097 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
1098 If ty involves a type function we may defer, which isn't very sensible.
1099 An egregious example of this was in test T9872a, which has a type signature
1100 Proxy :: Proxy (Solutions Cubes)
1101 Doing the ambiguity check on this signature generates the equality
1102 Solutions Cubes ~ Solutions Cubes
1103 and currently the constraint solver normalises both sides at vast cost.
1104 This little short-cut in 'defer' helps quite a bit.
1105
1106 Note [Care with type applications]
1107 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1108 Note: type applications need a bit of care!
1109 They can match FunTy and TyConApp, so use splitAppTy_maybe
1110 NB: we've already dealt with type variables and Notes,
1111 so if one type is an App the other one jolly well better be too
1112
1113 Note [Mismatched type lists and application decomposition]
1114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1115 When we find two TyConApps, you might think that the argument lists
1116 are guaranteed equal length. But they aren't. Consider matching
1117 w (T x) ~ Foo (T x y)
1118 We do match (w ~ Foo) first, but in some circumstances we simply create
1119 a deferred constraint; and then go ahead and match (T x ~ T x y).
1120 This came up in Trac #3950.
1121
1122 So either
1123 (a) either we must check for identical argument kinds
1124 when decomposing applications,
1125
1126 (b) or we must be prepared for ill-kinded unification sub-problems
1127
1128 Currently we adopt (b) since it seems more robust -- no need to maintain
1129 a global invariant.
1130
1131 Note [Expanding synonyms during unification]
1132 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1133 We expand synonyms during unification, but:
1134 * We expand *after* the variable case so that we tend to unify
1135 variables with un-expanded type synonym. This just makes it
1136 more likely that the inferred types will mention type synonyms
1137 understandable to the user
1138
1139 * We expand *before* the TyConApp case. For example, if we have
1140 type Phantom a = Int
1141 and are unifying
1142 Phantom Int ~ Phantom Char
1143 it is *wrong* to unify Int and Char.
1144
1145 * The problem case immediately above can happen only with arguments
1146 to the tycon. So we check for nullary tycons *before* expanding.
1147 This is particularly helpful when checking (* ~ *), because * is
1148 now a type synonym.
1149
1150 Note [Deferred Unification]
1151 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1152 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
1153 and yet its consistency is undetermined. Previously, there was no way to still
1154 make it consistent. So a mismatch error was issued.
1155
1156 Now these unifications are deferred until constraint simplification, where type
1157 family instances and given equations may (or may not) establish the consistency.
1158 Deferred unifications are of the form
1159 F ... ~ ...
1160 or x ~ ...
1161 where F is a type function and x is a type variable.
1162 E.g.
1163 id :: x ~ y => x -> y
1164 id e = e
1165
1166 involves the unification x = y. It is deferred until we bring into account the
1167 context x ~ y to establish that it holds.
1168
1169 If available, we defer original types (rather than those where closed type
1170 synonyms have already been expanded via tcCoreView). This is, as usual, to
1171 improve error messages.
1172
1173
1174 ************************************************************************
1175 * *
1176 uVar and friends
1177 * *
1178 ************************************************************************
1179
1180 @uVar@ is called when at least one of the types being unified is a
1181 variable. It does {\em not} assume that the variable is a fixed point
1182 of the substitution; rather, notice that @uVar@ (defined below) nips
1183 back into @uTys@ if it turns out that the variable is already bound.
1184 -}
1185
1186 uUnfilledVar :: CtOrigin
1187 -> TypeOrKind
1188 -> SwapFlag
1189 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1190 -> TcTauType -- Type 2
1191 -> TcM Coercion
1192 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
1193 -- It might be a skolem, or untouchable, or meta
1194
1195 uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2)
1196 | tv1 == tv2 -- Same type variable => no-op
1197 = return (mkNomReflCo (mkTyVarTy tv1))
1198
1199 | otherwise -- Distinct type variables
1200 = do { lookup2 <- lookupTcTyVar tv2
1201 ; case lookup2 of
1202 Filled ty2'
1203 -> uUnfilledVar origin t_or_k swapped tv1 details1 ty2'
1204 Unfilled details2
1205 -> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
1206 }
1207
1208 uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2
1209 -- ty2 is not a type variable
1210 = case details1 of
1211 MetaTv { mtv_ref = ref1 }
1212 -> do { dflags <- getDynFlags
1213 ; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2
1214 ; case mb_ty2' of
1215 Just (ty2', co_k) -> maybe_sym swapped <$>
1216 updateMeta tv1 ref1 ty2' co_k
1217 Nothing -> do { traceTc "Occ/type-family defer"
1218 (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
1219 $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
1220 ; defer }
1221 }
1222
1223 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
1224 where
1225 defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2
1226 -- Occurs check or an untouchable: just defer
1227 -- NB: occurs check isn't necessarily fatal:
1228 -- eg tv1 occured in type family parameter
1229
1230 ----------------
1231 uUnfilledVars :: CtOrigin
1232 -> TypeOrKind
1233 -> SwapFlag
1234 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1235 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
1236 -> TcM Coercion
1237 -- Invarant: The type variables are distinct,
1238 -- Neither is filled in yet
1239
1240 uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
1241 = do { traceTc "uUnfilledVars for" (ppr tv1 <+> text "and" <+> ppr tv2)
1242 ; traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1
1243 <+> text "with" <+> ppr k2)
1244 ; co_k <- uType kind_origin KindLevel k1 k2
1245 ; let no_swap ref = maybe_sym swapped <$>
1246 updateMeta tv1 ref ty2 (mkSymCo co_k)
1247 do_swap ref = maybe_sym (flipSwap swapped) <$>
1248 updateMeta tv2 ref ty1 co_k
1249 ; case (details1, details2) of
1250 { ( MetaTv { mtv_info = i1, mtv_ref = ref1 }
1251 , MetaTv { mtv_info = i2, mtv_ref = ref2 } )
1252 | nicer_to_update_tv1 tv1 i1 i2 -> no_swap ref1
1253 | otherwise -> do_swap ref2
1254 ; (MetaTv { mtv_ref = ref1 }, _) -> no_swap ref1
1255 ; (_, MetaTv { mtv_ref = ref2 }) -> do_swap ref2
1256
1257 -- Can't do it in-place, so defer
1258 -- This happens for skolems of all sorts
1259 ; _ -> do { traceTc "deferring because I can't find a meta-tyvar:"
1260 (pprTcTyVarDetails details1 <+> pprTcTyVarDetails details2)
1261 ; unSwap swapped (uType_defer origin t_or_k) ty1 ty2 } } }
1262 where
1263 k1 = tyVarKind tv1
1264 k2 = tyVarKind tv2
1265 ty1 = mkTyVarTy tv1
1266 ty2 = mkTyVarTy tv2
1267 kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
1268
1269 -- | apply sym iff swapped
1270 maybe_sym :: SwapFlag -> Coercion -> Coercion
1271 maybe_sym IsSwapped = mkSymCo
1272 maybe_sym NotSwapped = id
1273
1274 nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
1275 nicer_to_update_tv1 _ _ SigTv = True
1276 nicer_to_update_tv1 _ SigTv _ = False
1277 -- Try not to update SigTvs; and try to update sys-y type
1278 -- variables in preference to ones gotten (say) by
1279 -- instantiating a polymorphic function with a user-written
1280 -- type sig
1281 nicer_to_update_tv1 _ ReturnTv _ = True
1282 nicer_to_update_tv1 _ _ ReturnTv = False
1283 -- ReturnTvs are really holes just begging to be filled in.
1284 -- Let's oblige.
1285 nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1)
1286
1287 ----------------
1288 checkTauTvUpdate :: DynFlags
1289 -> CtOrigin
1290 -> TypeOrKind
1291 -> TcTyVar -- tv :: k1
1292 -> TcType -- ty :: k2
1293 -> TcM (Maybe ( TcType -- possibly-expanded ty
1294 , Coercion )) -- :: k2 ~N k1
1295 -- (checkTauTvUpdate tv ty)
1296 -- We are about to update the TauTv/ReturnTv tv with ty.
1297 -- Check (a) that tv doesn't occur in ty (occurs check)
1298 -- (b) that kind(ty) is a sub-kind of kind(tv)
1299 --
1300 -- We have two possible outcomes:
1301 -- (1) Return the type to update the type variable with,
1302 -- [we know the update is ok]
1303 -- (2) Return Nothing,
1304 -- [the update might be dodgy]
1305 --
1306 -- Note that "Nothing" does not mean "definite error". For example
1307 -- type family F a
1308 -- type instance F Int = Int
1309 -- consider
1310 -- a ~ F a
1311 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
1312 -- we return Nothing, leaving it to the later constraint simplifier to
1313 -- sort matters out.
1314
1315 checkTauTvUpdate dflags origin t_or_k tv ty
1316 | SigTv <- info
1317 = ASSERT( not (isTyVarTy ty) )
1318 return Nothing
1319 | otherwise
1320 = do { ty <- zonkTcType ty
1321 ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
1322 ; if | is_return_tv -> -- ReturnTv: a simple occurs-check is all that we need
1323 -- See Note [ReturnTv] in TcType
1324 if tv `elemVarSet` tyCoVarsOfType ty
1325 then return Nothing
1326 else return (Just (ty, co_k))
1327 | defer_me ty -> -- Quick test
1328 -- Failed quick test so try harder
1329 case occurCheckExpand dflags tv ty of
1330 OC_OK ty2 | defer_me ty2 -> return Nothing
1331 | otherwise -> return (Just (ty2, co_k))
1332 _ -> return Nothing
1333 | otherwise -> return (Just (ty, co_k)) }
1334 where
1335 kind_origin = KindEqOrigin (mkTyVarTy tv) ty origin (Just t_or_k)
1336 details = tcTyVarDetails tv
1337 info = mtv_info details
1338 is_return_tv = isReturnTyVar tv
1339 impredicative = canUnifyWithPolyType dflags details
1340
1341 defer_me :: TcType -> Bool
1342 -- Checks for (a) occurrence of tv
1343 -- (b) type family applications
1344 -- (c) foralls
1345 -- See Note [Conservative unification check]
1346 defer_me (LitTy {}) = False
1347 defer_me (TyVarTy tv') = tv == tv'
1348 defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
1349 || not (impredicative || isTauTyCon tc)
1350 defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t
1351 || (isNamedBinder bndr && not impredicative)
1352 defer_me (AppTy fun arg) = defer_me fun || defer_me arg
1353 defer_me (CastTy ty co) = defer_me ty || defer_me_co co
1354 defer_me (CoercionTy co) = defer_me_co co
1355
1356 -- We don't really care if there are type families in a coercion,
1357 -- but we still can't have an occurs-check failure
1358 defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
1359
1360 {-
1361 Note [Conservative unification check]
1362 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1363 When unifying (tv ~ rhs), w try to avoid creating deferred constraints
1364 only for efficiency. However, we do not unify (the defer_me check) if
1365 a) There's an occurs check (tv is in fvs(rhs))
1366 b) There's a type-function call in 'rhs'
1367
1368 If we fail defer_me we use occurCheckExpand to try to make it pass,
1369 (see Note [Type synonyms and the occur check]) and then use defer_me
1370 again to check. Example: Trac #4917)
1371 a ~ Const a b
1372 where type Const a b = a. We can solve this immediately, even when
1373 'a' is a skolem, just by expanding the synonym.
1374
1375 We always defer type-function calls, even if it's be perfectly safe to
1376 unify, eg (a ~ F [b]). Reason: this ensures that the constraint
1377 solver gets to see, and hence simplify the type-function call, which
1378 in turn might simplify the type of an inferred function. Test ghci046
1379 is a case in point.
1380
1381 More mysteriously, test T7010 gave a horrible error
1382 T7010.hs:29:21:
1383 Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
1384 Expected type: (ValueTuple Vector, ValueTuple Vector)
1385 Actual type: (ValueTuple Vector, ValueTuple Vector)
1386 because an insoluble type function constraint got mixed up with
1387 a soluble one when flattening. I never fully understood this, but
1388 deferring type-function applications made it go away :-(.
1389 T5853 also got a less-good error message with more aggressive
1390 unification of type functions.
1391
1392 Moreover the Note [Type family sharing] gives another reason, but
1393 again I'm not sure if it's really valid.
1394
1395 Note [Type synonyms and the occur check]
1396 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1397 Generally speaking we try to update a variable with type synonyms not
1398 expanded, which improves later error messages, unless looking
1399 inside a type synonym may help resolve a spurious occurs check
1400 error. Consider:
1401 type A a = ()
1402
1403 f :: (A a -> a -> ()) -> ()
1404 f = \ _ -> ()
1405
1406 x :: ()
1407 x = f (\ x p -> p x)
1408
1409 We will eventually get a constraint of the form t ~ A t. The ok function above will
1410 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1411 unified with the original type A t, we would lead the type checker into an infinite loop.
1412
1413 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1414 the ok function expands the synonym to detect opportunities for occurs check success using
1415 the underlying definition of the type synonym.
1416
1417 The same applies later on in the constraint interaction code; see TcInteract,
1418 function @occ_check_ok@.
1419
1420 Note [Type family sharing]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 We must avoid eagerly unifying type variables to types that contain function symbols,
1423 because this may lead to loss of sharing, and in turn, in very poor performance of the
1424 constraint simplifier. Assume that we have a wanted constraint:
1425 {
1426 m1 ~ [F m2],
1427 m2 ~ [F m3],
1428 m3 ~ [F m4],
1429 D m1,
1430 D m2,
1431 D m3
1432 }
1433 where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
1434 then, after zonking, our constraint simplifier will be faced with the following wanted
1435 constraint:
1436 {
1437 D [F [F [F m4]]],
1438 D [F [F m4]],
1439 D [F m4]
1440 }
1441 which has to be flattened by the constraint solver. In the absence of
1442 a flat-cache, this may generate a polynomially larger number of
1443 flatten skolems and the constraint sets we are working with will be
1444 polynomially larger.
1445
1446 Instead, if we defer the unifications m1 := [F m2], etc. we will only
1447 be generating three flatten skolems, which is the maximum possible
1448 sharing arising from the original constraint. That's why we used to
1449 use a local "ok" function, a variant of TcType.occurCheckExpand.
1450
1451 HOWEVER, we *do* now have a flat-cache, which effectively recovers the
1452 sharing, so there's no great harm in losing it -- and it's generally
1453 more efficient to do the unification up-front.
1454
1455 Note [Non-TcTyVars in TcUnify]
1456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1457 Because the same code is now shared between unifying types and unifying
1458 kinds, we sometimes will see proper TyVars floating around the unifier.
1459 Example (from test case polykinds/PolyKinds12):
1460
1461 type family Apply (f :: k1 -> k2) (x :: k1) :: k2
1462 type instance Apply g y = g y
1463
1464 When checking the instance declaration, we first *kind-check* the LHS
1465 and RHS, discovering that the instance really should be
1466
1467 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
1468
1469 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
1470 as a second pass, we desugar the RHS (which is done in functions prefixed
1471 with "tc" in TcTyClsDecls"). By this time, all the kind-vars are proper
1472 TyVars, not TcTyVars, get some kind unification must happen.
1473
1474 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
1475 meta-tyvar.
1476
1477 This used to not be necessary for type-checking (that is, before * :: *)
1478 because expressions get desugared via an algorithm separate from
1479 type-checking (with wrappers, etc.). Types get desugared very differently,
1480 causing this wibble in behavior seen here.
1481 -}
1482
1483 data LookupTyVarResult -- The result of a lookupTcTyVar call
1484 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1485 | Filled TcType
1486
1487 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1488 lookupTcTyVar tyvar
1489 | MetaTv { mtv_ref = ref } <- details
1490 = do { meta_details <- readMutVar ref
1491 ; case meta_details of
1492 Indirect ty -> return (Filled ty)
1493 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1494 -- Note [Unifying untouchables]
1495 ; if is_touchable then
1496 return (Unfilled details)
1497 else
1498 return (Unfilled vanillaSkolemTv) } }
1499 | otherwise
1500 = return (Unfilled details)
1501 where
1502 details = tcTyVarDetails tyvar
1503
1504 -- | Fill in a meta-tyvar
1505 updateMeta :: TcTyVar -- ^ tv to fill in, tv :: k1
1506 -> TcRef MetaDetails -- ^ ref to tv's metadetails
1507 -> TcType -- ^ ty2 :: k2
1508 -> Coercion -- ^ kind_co :: k2 ~N k1
1509 -> TcM Coercion -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
1510 updateMeta tv1 ref1 ty2 kind_co
1511 = do { let ty2_refl = mkNomReflCo ty2
1512 (ty2', co) = ( ty2 `mkCastTy` kind_co
1513 , mkCoherenceLeftCo ty2_refl kind_co )
1514 ; writeMetaTyVarRef tv1 ref1 ty2'
1515 ; return co }
1516
1517 {-
1518 Note [Unifying untouchables]
1519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1520 We treat an untouchable type variable as if it was a skolem. That
1521 ensures it won't unify with anything. It's a slight had, because
1522 we return a made-up TcTyVarDetails, but I think it works smoothly.
1523 -}
1524
1525 -- | Breaks apart a function kind into its pieces.
1526 matchExpectedFunKind :: Arity -- ^ # of args remaining, only for errors
1527 -> TcType -- ^ type, only for errors
1528 -> TcKind -- ^ function kind
1529 -> TcM (Coercion, TcKind, TcKind)
1530 -- ^ co :: old_kind ~ arg -> res
1531 matchExpectedFunKind num_args_remaining ty = go
1532 where
1533 go k | Just k' <- coreView k = go k'
1534
1535 go k@(TyVarTy kvar)
1536 | isTcTyVar kvar, isMetaTyVar kvar
1537 = do { maybe_kind <- readMetaTyVar kvar
1538 ; case maybe_kind of
1539 Indirect fun_kind -> go fun_kind
1540 Flexi -> defer (isReturnTyVar kvar) k }
1541
1542 go k@(ForAllTy (Anon arg) res)
1543 = return (mkNomReflCo k, arg, res)
1544
1545 go other = defer False other
1546
1547 defer is_return k
1548 = do { arg_kind <- new_flexi
1549 ; res_kind <- new_flexi
1550 ; let new_fun = mkFunTy arg_kind res_kind
1551 thing = mkTypeErrorThingArgs ty num_args_remaining
1552 origin = TypeEqOrigin { uo_actual = k
1553 , uo_expected = new_fun
1554 , uo_thing = Just thing
1555 }
1556 ; co <- uType origin KindLevel k new_fun
1557 ; return (co, arg_kind, res_kind) }
1558 where
1559 new_flexi | is_return = newReturnTyVarTy liftedTypeKind
1560 | otherwise = newMetaKindVar