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