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