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