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