Small changes to ddump-tc tracing
[ghc.git] / compiler / typecheck / TcUnify.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Type subsumption and unification
7 -}
8
9 {-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
10
11 module TcUnify (
12 -- Full-blown subsumption
13 tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
14 tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
15 tcSubTypeDS_NC_O, tcSubTypeET,
16 checkConstraints, buildImplicationFor,
17
18 -- Various unifications
19 unifyType, unifyTheta, unifyKind,
20 uType, promoteTcType,
21 swapOverTyVars, canSolveByUnification,
22
23 --------------------------------
24 -- Holes
25 tcInferInst, tcInferNoInst,
26 matchExpectedListTy,
27 matchExpectedPArrTy,
28 matchExpectedTyConApp,
29 matchExpectedAppTy,
30 matchExpectedFunTys,
31 matchActualFunTys, matchActualFunTysPart,
32 matchExpectedFunKind,
33
34 wrapFunResCoercion,
35
36 occCheckExpand, metaTyVarUpdateOK,
37 occCheckForErrors, OccCheckResult(..)
38
39 ) where
40
41 #include "HsVersions.h"
42
43 import HsSyn
44 import TyCoRep
45 import TcMType
46 import TcRnMonad
47 import TcType
48 import Type
49 import Coercion
50 import TcEvidence
51 import Name ( isSystemName )
52 import Inst
53 import TyCon
54 import TysWiredIn
55 import TysPrim( tYPE )
56 import Var
57 import VarSet
58 import VarEnv
59 import ErrUtils
60 import DynFlags
61 import BasicTypes
62 import Bag
63 import Util
64 import Pair( pFst )
65 import qualified GHC.LanguageExtensions as LangExt
66 import Outputable
67 import FastString
68
69 import Control.Monad
70 import Control.Arrow ( second )
71
72 {-
73 ************************************************************************
74 * *
75 matchExpected functions
76 * *
77 ************************************************************************
78
79 Note [Herald for matchExpectedFunTys]
80 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
81 The 'herald' always looks like:
82 "The equation(s) for 'f' have"
83 "The abstraction (\x.e) takes"
84 "The section (+ x) expects"
85 "The function 'f' is applied to"
86
87 This is used to construct a message of form
88
89 The abstraction `\Just 1 -> ...' takes two arguments
90 but its type `Maybe a -> a' has only one
91
92 The equation(s) for `f' have two arguments
93 but its type `Maybe a -> a' has only one
94
95 The section `(f 3)' requires 'f' to take two arguments
96 but its type `Int -> Int' has only one
97
98 The function 'f' is applied to two arguments
99 but its type `Int -> Int' has only one
100
101 When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
102 picture, we have a choice in deciding whether to count the type applications as
103 proper arguments:
104
105 The function 'f' is applied to one visible type argument
106 and two value arguments
107 but its type `forall a. a -> a` has only one visible type argument
108 and one value argument
109
110 Or whether to include the type applications as part of the herald itself:
111
112 The expression 'f @Int' is applied to two arguments
113 but its type `Int -> Int` has only one
114
115 The latter is easier to implement and is arguably easier to understand, so we
116 choose to implement that option.
117
118 Note [matchExpectedFunTys]
119 ~~~~~~~~~~~~~~~~~~~~~~~~~~
120 matchExpectedFunTys checks that a sigma has the form
121 of an n-ary function. It passes the decomposed type to the
122 thing_inside, and returns a wrapper to coerce between the two types
123
124 It's used wherever a language construct must have a functional type,
125 namely:
126 A lambda expression
127 A function definition
128 An operator section
129
130 This function must be written CPS'd because it needs to fill in the
131 ExpTypes produced for arguments before it can fill in the ExpType
132 passed in.
133
134 -}
135
136 -- Use this one when you have an "expected" type.
137 matchExpectedFunTys :: forall a.
138 SDoc -- See Note [Herald for matchExpectedFunTys]
139 -> Arity
140 -> ExpRhoType -- deeply skolemised
141 -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
142 -- must fill in these ExpTypes here
143 -> TcM (a, HsWrapper)
144 -- If matchExpectedFunTys n ty = (_, wrap)
145 -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
146 -- where [t1, ..., tn], ty_r are passed to the thing_inside
147 matchExpectedFunTys herald arity orig_ty thing_inside
148 = case orig_ty of
149 Check ty -> go [] arity ty
150 _ -> defer [] arity orig_ty
151 where
152 go acc_arg_tys 0 ty
153 = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty)
154 ; return (result, idHsWrapper) }
155
156 go acc_arg_tys n ty
157 | Just ty' <- tcView ty = go acc_arg_tys n ty'
158
159 go acc_arg_tys n (FunTy arg_ty res_ty)
160 = ASSERT( not (isPredTy arg_ty) )
161 do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
162 (n-1) res_ty
163 ; return ( result
164 , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) }
165 where
166 doc = text "When inferring the argument type of a function with type" <+>
167 quotes (ppr orig_ty)
168
169 go acc_arg_tys n ty@(TyVarTy tv)
170 | isMetaTyVar tv
171 = do { cts <- readMetaTyVar tv
172 ; case cts of
173 Indirect ty' -> go acc_arg_tys n ty'
174 Flexi -> defer acc_arg_tys n (mkCheckExpType ty) }
175
176 -- In all other cases we bale out into ordinary unification
177 -- However unlike the meta-tyvar case, we are sure that the
178 -- number of arguments doesn't match arity of the original
179 -- type, so we can add a bit more context to the error message
180 -- (cf Trac #7869).
181 --
182 -- It is not always an error, because specialized type may have
183 -- different arity, for example:
184 --
185 -- > f1 = f2 'a'
186 -- > f2 :: Monad m => m Bool
187 -- > f2 = undefined
188 --
189 -- But in that case we add specialized type into error context
190 -- anyway, because it may be useful. See also Trac #9605.
191 go acc_arg_tys n ty = addErrCtxtM mk_ctxt $
192 defer acc_arg_tys n (mkCheckExpType ty)
193
194 ------------
195 defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
196 defer acc_arg_tys n fun_ty
197 = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
198 ; res_ty <- newInferExpTypeInst
199 ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
200 ; more_arg_tys <- mapM readExpType more_arg_tys
201 ; res_ty <- readExpType res_ty
202 ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
203 ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
204 -- Not a good origin at all :-(
205 ; return (result, wrap) }
206
207 ------------
208 mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
209 mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_tc_ty
210 ; let (args, _) = tcSplitFunTys ty
211 n_actual = length args
212 (env'', orig_ty') = tidyOpenType env' orig_tc_ty
213 ; return ( env''
214 , mk_fun_tys_msg orig_ty' ty n_actual arity herald) }
215 where
216 orig_tc_ty = checkingExpType "matchExpectedFunTys" orig_ty
217 -- this is safe b/c we're called from "go"
218
219 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
220 -- for example in function application
221 matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
222 -> CtOrigin
223 -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType
224 -> Arity
225 -> TcSigmaType
226 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
227 -- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
228 -- then wrap : ty ~> (t1 -> ... -> tn -> ty_r)
229 matchActualFunTys herald ct_orig mb_thing arity ty
230 = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
231
232 -- | Variant of 'matchActualFunTys' that works when supplied only part
233 -- (that is, to the right of some arrows) of the full function type
234 matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
235 -> CtOrigin
236 -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType
237 -> Arity
238 -> TcSigmaType
239 -> [TcSigmaType] -- reversed args. See (*) below.
240 -> Arity -- overall arity of the function, for errs
241 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
242 matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
243 orig_old_args full_arity
244 = go arity orig_old_args orig_ty
245 -- Does not allocate unnecessary meta variables: if the input already is
246 -- a function, we just take it apart. Not only is this efficient,
247 -- it's important for higher rank: the argument might be of form
248 -- (forall a. ty) -> other
249 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
250 -- hide the forall inside a meta-variable
251
252 -- (*) Sometimes it's necessary to call matchActualFunTys with only part
253 -- (that is, to the right of some arrows) of the type of the function in
254 -- question. (See TcExpr.tcArgs.) This argument is the reversed list of
255 -- arguments already seen (that is, not part of the TcSigmaType passed
256 -- in elsewhere).
257
258 where
259 -- This function has a bizarre mechanic: it accumulates arguments on
260 -- the way down and also builds an argument list on the way up. Why:
261 -- 1. The returns args list and the accumulated args list might be different.
262 -- The accumulated args include all the arg types for the function,
263 -- including those from before this function was called. The returned
264 -- list should include only those arguments produced by this call of
265 -- matchActualFunTys
266 --
267 -- 2. The HsWrapper can be built only on the way up. It seems (more)
268 -- bizarre to build the HsWrapper but not the arg_tys.
269 --
270 -- Refactoring is welcome.
271 go :: Arity
272 -> [TcSigmaType] -- accumulator of arguments (reversed)
273 -> TcSigmaType -- the remainder of the type as we're processing
274 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
275 go 0 _ ty = return (idHsWrapper, [], ty)
276
277 go n acc_args ty
278 | not (null tvs && null theta)
279 = do { (wrap1, rho) <- topInstantiate ct_orig ty
280 ; (wrap2, arg_tys, res_ty) <- go n acc_args rho
281 ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
282 where
283 (tvs, theta, _) = tcSplitSigmaTy ty
284
285 go n acc_args ty
286 | Just ty' <- tcView ty = go n acc_args ty'
287
288 go n acc_args (FunTy arg_ty res_ty)
289 = ASSERT( not (isPredTy arg_ty) )
290 do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
291 ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
292 , arg_ty : tys, ty_r ) }
293 where
294 doc = text "When inferring the argument type of a function with type" <+>
295 quotes (ppr orig_ty)
296
297 go n acc_args ty@(TyVarTy tv)
298 | isMetaTyVar tv
299 = do { cts <- readMetaTyVar tv
300 ; case cts of
301 Indirect ty' -> go n acc_args ty'
302 Flexi -> defer n ty }
303
304 -- In all other cases we bale out into ordinary unification
305 -- However unlike the meta-tyvar case, we are sure that the
306 -- number of arguments doesn't match arity of the original
307 -- type, so we can add a bit more context to the error message
308 -- (cf Trac #7869).
309 --
310 -- It is not always an error, because specialized type may have
311 -- different arity, for example:
312 --
313 -- > f1 = f2 'a'
314 -- > f2 :: Monad m => m Bool
315 -- > f2 = undefined
316 --
317 -- But in that case we add specialized type into error context
318 -- anyway, because it may be useful. See also Trac #9605.
319 go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
320 defer n ty
321
322 ------------
323 defer n fun_ty
324 = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
325 ; res_ty <- newOpenFlexiTyVarTy
326 ; let unif_fun_ty = mkFunTys arg_tys res_ty
327 ; co <- unifyType mb_thing fun_ty unif_fun_ty
328 ; return (mkWpCastN co, arg_tys, res_ty) }
329
330 ------------
331 mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
332 mk_ctxt arg_tys res_ty env
333 = do { let ty = mkFunTys arg_tys res_ty
334 ; (env1, zonked) <- zonkTidyTcType env ty
335 -- zonking might change # of args
336 ; let (zonked_args, _) = tcSplitFunTys zonked
337 n_actual = length zonked_args
338 (env2, unzonked) = tidyOpenType env1 ty
339 ; return ( env2
340 , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) }
341
342 mk_fun_tys_msg :: TcType -- the full type passed in (unzonked)
343 -> TcType -- the full type passed in (zonked)
344 -> Arity -- the # of args found
345 -> Arity -- the # of args wanted
346 -> SDoc -- overall herald
347 -> SDoc
348 mk_fun_tys_msg full_ty ty n_args full_arity herald
349 = herald <+> speakNOf full_arity (text "argument") <> comma $$
350 if n_args == full_arity
351 then text "its type is" <+> quotes (pprType full_ty) <>
352 comma $$
353 text "it is specialized to" <+> quotes (pprType ty)
354 else sep [text "but its type" <+> quotes (pprType ty),
355 if n_args == 0 then text "has none"
356 else text "has only" <+> speakN n_args]
357
358 ----------------------
359 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
360 -- Special case for lists
361 matchExpectedListTy exp_ty
362 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
363 ; return (co, elt_ty) }
364
365 ----------------------
366 matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
367 -- Special case for parrs
368 matchExpectedPArrTy exp_ty
369 = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
370 ; return (co, elt_ty) }
371
372 ---------------------
373 matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
374 -> TcRhoType -- orig_ty
375 -> TcM (TcCoercionN, -- T k1 k2 k3 a b c ~N orig_ty
376 [TcSigmaType]) -- Element types, k1 k2 k3 a b c
377
378 -- It's used for wired-in tycons, so we call checkWiredInTyCon
379 -- Precondition: never called with FunTyCon
380 -- Precondition: input type :: *
381 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
382
383 matchExpectedTyConApp tc orig_ty
384 = ASSERT(tc /= funTyCon) go orig_ty
385 where
386 go ty
387 | Just ty' <- tcView ty
388 = go ty'
389
390 go ty@(TyConApp tycon args)
391 | tc == tycon -- Common case
392 = return (mkTcNomReflCo ty, args)
393
394 go (TyVarTy tv)
395 | isMetaTyVar tv
396 = do { cts <- readMetaTyVar tv
397 ; case cts of
398 Indirect ty -> go ty
399 Flexi -> defer }
400
401 go _ = defer
402
403 -- If the common case does not occur, instantiate a template
404 -- T k1 .. kn t1 .. tm, and unify with the original type
405 -- Doing it this way ensures that the types we return are
406 -- kind-compatible with T. For example, suppose we have
407 -- matchExpectedTyConApp T (f Maybe)
408 -- where data T a = MkT a
409 -- Then we don't want to instantiate T's data constructors with
410 -- (a::*) ~ Maybe
411 -- because that'll make types that are utterly ill-kinded.
412 -- This happened in Trac #7368
413 defer
414 = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
415 ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
416 ; let args = mkTyVarTys arg_tvs
417 tc_template = mkTyConApp tc args
418 ; co <- unifyType Nothing tc_template orig_ty
419 ; return (co, args) }
420
421 ----------------------
422 matchExpectedAppTy :: TcRhoType -- orig_ty
423 -> TcM (TcCoercion, -- m a ~N orig_ty
424 (TcSigmaType, TcSigmaType)) -- Returns m, a
425 -- If the incoming type is a mutable type variable of kind k, then
426 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
427
428 matchExpectedAppTy orig_ty
429 = go orig_ty
430 where
431 go ty
432 | Just ty' <- tcView ty = go ty'
433
434 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
435 = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
436
437 go (TyVarTy tv)
438 | isMetaTyVar tv
439 = do { cts <- readMetaTyVar tv
440 ; case cts of
441 Indirect ty -> go ty
442 Flexi -> defer }
443
444 go _ = defer
445
446 -- Defer splitting by generating an equality constraint
447 defer
448 = do { ty1 <- newFlexiTyVarTy kind1
449 ; ty2 <- newFlexiTyVarTy kind2
450 ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
451 ; return (co, (ty1, ty2)) }
452
453 orig_kind = typeKind orig_ty
454 kind1 = mkFunTy liftedTypeKind orig_kind
455 kind2 = liftedTypeKind -- m :: * -> k
456 -- arg type :: *
457
458 {-
459 ************************************************************************
460 * *
461 Subsumption checking
462 * *
463 ************************************************************************
464
465 Note [Subsumption checking: tcSubType]
466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
467 All the tcSubType calls have the form
468 tcSubType actual_ty expected_ty
469 which checks
470 actual_ty <= expected_ty
471
472 That is, that a value of type actual_ty is acceptable in
473 a place expecting a value of type expected_ty. I.e. that
474
475 actual ty is more polymorphic than expected_ty
476
477 It returns a coercion function
478 co_fn :: actual_ty ~ expected_ty
479 which takes an HsExpr of type actual_ty into one of type
480 expected_ty.
481
482 These functions do not actually check for subsumption. They check if
483 expected_ty is an appropriate annotation to use for something of type
484 actual_ty. This difference matters when thinking about visible type
485 application. For example,
486
487 forall a. a -> forall b. b -> b
488 DOES NOT SUBSUME
489 forall a b. a -> b -> b
490
491 because the type arguments appear in a different order. (Neither does
492 it work the other way around.) BUT, these types are appropriate annotations
493 for one another. Because the user directs annotations, it's OK if some
494 arguments shuffle around -- after all, it's what the user wants.
495 Bottom line: none of this changes with visible type application.
496
497 There are a number of wrinkles (below).
498
499 Notice that Wrinkle 1 and 2 both require eta-expansion, which technically
500 may increase termination. We just put up with this, in exchange for getting
501 more predictable type inference.
502
503 Wrinkle 1: Note [Deep skolemisation]
504 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
505 We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a)
506 (see section 4.6 of "Practical type inference for higher rank types")
507 So we must deeply-skolemise the RHS before we instantiate the LHS.
508
509 That is why tc_sub_type starts with a call to tcSkolemise (which does the
510 deep skolemisation), and then calls the DS variant (which assumes
511 that expected_ty is deeply skolemised)
512
513 Wrinkle 2: Note [Co/contra-variance of subsumption checking]
514 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
515 Consider g :: (Int -> Int) -> Int
516 f1 :: (forall a. a -> a) -> Int
517 f1 = g
518
519 f2 :: (forall a. a -> a) -> Int
520 f2 x = g x
521 f2 will typecheck, and it would be odd/fragile if f1 did not.
522 But f1 will only typecheck if we have that
523 (Int->Int) -> Int <= (forall a. a->a) -> Int
524 And that is only true if we do the full co/contravariant thing
525 in the subsumption check. That happens in the FunTy case of
526 tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
527 HsWrapper.
528
529 Another powerful reason for doing this co/contra stuff is visible
530 in Trac #9569, involving instantiation of constraint variables,
531 and again involving eta-expansion.
532
533 Wrinkle 3: Note [Higher rank types]
534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
535 Consider tc150:
536 f y = \ (x::forall a. a->a). blah
537 The following happens:
538 * We will infer the type of the RHS, ie with a res_ty = alpha.
539 * Then the lambda will split alpha := beta -> gamma.
540 * And then we'll check tcSubType IsSwapped beta (forall a. a->a)
541
542 So it's important that we unify beta := forall a. a->a, rather than
543 skolemising the type.
544 -}
545
546
547 -- | Call this variant when you are in a higher-rank situation and
548 -- you know the right-hand type is deeply skolemised.
549 tcSubTypeHR :: CtOrigin -- ^ of the actual type
550 -> Maybe (HsExpr GhcRn) -- ^ If present, it has type ty_actual
551 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
552 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
553
554 ------------------------
555 tcSubTypeET :: CtOrigin -> UserTypeCtxt
556 -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
557 -- If wrap = tc_sub_type_et t1 t2
558 -- => wrap :: t1 ~> t2
559 tcSubTypeET orig ctxt (Check ty_actual) ty_expected
560 = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
561 where
562 eq_orig = TypeEqOrigin { uo_actual = ty_expected
563 , uo_expected = ty_actual
564 , uo_thing = Nothing
565 , uo_visible = True }
566
567 tcSubTypeET _ _ (Infer inf_res) ty_expected
568 = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
569 do { co <- fillInferResult ty_expected inf_res
570 ; return (mkWpCastN (mkTcSymCo co)) }
571
572 ------------------------
573 tcSubTypeO :: CtOrigin -- ^ of the actual type
574 -> UserTypeCtxt -- ^ of the expected type
575 -> TcSigmaType
576 -> ExpRhoType
577 -> TcM HsWrapper
578 tcSubTypeO orig ctxt ty_actual ty_expected
579 = addSubTypeCtxt ty_actual ty_expected $
580 do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
581 , pprUserTypeCtxt ctxt
582 , ppr ty_actual
583 , ppr ty_expected ])
584 ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
585
586 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
587 addSubTypeCtxt ty_actual ty_expected thing_inside
588 | isRhoTy ty_actual -- If there is no polymorphism involved, the
589 , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions)
590 = thing_inside -- gives enough context by itself
591 | otherwise
592 = addErrCtxtM mk_msg thing_inside
593 where
594 mk_msg tidy_env
595 = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual
596 -- might not be filled if we're debugging. ugh.
597 ; mb_ty_expected <- readExpType_maybe ty_expected
598 ; (tidy_env, ty_expected) <- case mb_ty_expected of
599 Just ty -> second mkCheckExpType <$>
600 zonkTidyTcType tidy_env ty
601 Nothing -> return (tidy_env, ty_expected)
602 ; ty_expected <- readExpType ty_expected
603 ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
604 ; let msg = vcat [ hang (text "When checking that:")
605 4 (ppr ty_actual)
606 , nest 2 (hang (text "is more polymorphic than:")
607 2 (ppr ty_expected)) ]
608 ; return (tidy_env, msg) }
609
610 ---------------
611 -- The "_NC" variants do not add a typechecker-error context;
612 -- the caller is assumed to do that
613
614 tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
615 -- Checks that actual <= expected
616 -- Returns HsWrapper :: actual ~ expected
617 tcSubType_NC ctxt ty_actual ty_expected
618 = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
619 ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected }
620 where
621 origin = TypeEqOrigin { uo_actual = ty_actual
622 , uo_expected = ty_expected
623 , uo_thing = Nothing
624 , uo_visible = True }
625
626 tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
627 -- Just like tcSubType, but with the additional precondition that
628 -- ty_expected is deeply skolemised (hence "DS")
629 tcSubTypeDS orig ctxt ty_actual ty_expected
630 = addSubTypeCtxt ty_actual ty_expected $
631 do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
632 ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
633
634 tcSubTypeDS_NC_O :: CtOrigin -- origin used for instantiation only
635 -> UserTypeCtxt
636 -> Maybe (HsExpr GhcRn)
637 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
638 -- Just like tcSubType, but with the additional precondition that
639 -- ty_expected is deeply skolemised
640 tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
641 = case ty_expected of
642 Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res
643 Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
644 where
645 eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
646 , uo_thing = ppr <$> m_thing
647 , uo_visible = True }
648
649 ---------------
650 tc_sub_tc_type :: CtOrigin -- used when calling uType
651 -> CtOrigin -- used when instantiating
652 -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
653 -- If wrap = tc_sub_type t1 t2
654 -- => wrap :: t1 ~> t2
655 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
656 | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
657 , not (possibly_poly ty_actual)
658 = do { traceTc "tc_sub_tc_type (drop to equality)" $
659 vcat [ text "ty_actual =" <+> ppr ty_actual
660 , text "ty_expected =" <+> ppr ty_expected ]
661 ; mkWpCastN <$>
662 uType TypeLevel eq_orig ty_actual ty_expected }
663
664 | otherwise -- This is the general case
665 = do { traceTc "tc_sub_tc_type (general case)" $
666 vcat [ text "ty_actual =" <+> ppr ty_actual
667 , text "ty_expected =" <+> ppr ty_expected ]
668 ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
669 \ _ sk_rho ->
670 tc_sub_type_ds eq_orig inst_orig ctxt
671 ty_actual sk_rho
672 ; return (sk_wrap <.> inner_wrap) }
673 where
674 possibly_poly ty
675 | isForAllTy ty = True
676 | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
677 | otherwise = False
678 -- NB *not* tcSplitFunTy, because here we want
679 -- to decompose type-class arguments too
680
681 definitely_poly ty
682 | (tvs, theta, tau) <- tcSplitSigmaTy ty
683 , (tv:_) <- tvs
684 , null theta
685 , isInsolubleOccursCheck NomEq tv tau
686 = True
687 | otherwise
688 = False
689
690 {- Note [Don't skolemise unnecessarily]
691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
692 Suppose we are trying to solve
693 (Char->Char) <= (forall a. a->a)
694 We could skolemise the 'forall a', and then complain
695 that (Char ~ a) is insoluble; but that's a pretty obscure
696 error. It's better to say that
697 (Char->Char) ~ (forall a. a->a)
698 fails.
699
700 So roughly:
701 * if the ty_expected has an outermost forall
702 (i.e. skolemisation is the next thing we'd do)
703 * and the ty_actual has no top-level polymorphism (but looking deeply)
704 then we can revert to simple equality. But we need to be careful.
705 These examples are all fine:
706
707 * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
708 Polymorphism is buried in ty_actual
709
710 * (Char->Char) <= (forall a. Char -> Char)
711 ty_expected isn't really polymorphic
712
713 * (Char->Char) <= (forall a. (a~Char) => a -> a)
714 ty_expected isn't really polymorphic
715
716 * (Char->Char) <= (forall a. F [a] Char -> Char)
717 where type instance F [x] t = t
718 ty_expected isn't really polymorphic
719
720 If we prematurely go to equality we'll reject a program we should
721 accept (e.g. Trac #13752). So the test (which is only to improve
722 error message) is very conservative:
723 * ty_actual is /definitely/ monomorphic
724 * ty_expected is /definitely/ polymorphic
725 -}
726
727 ---------------
728 tc_sub_type_ds :: CtOrigin -- used when calling uType
729 -> CtOrigin -- used when instantiating
730 -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
731 -- If wrap = tc_sub_type_ds t1 t2
732 -- => wrap :: t1 ~> t2
733 -- Here is where the work actually happens!
734 -- Precondition: ty_expected is deeply skolemised
735 tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
736 = do { traceTc "tc_sub_type_ds" $
737 vcat [ text "ty_actual =" <+> ppr ty_actual
738 , text "ty_expected =" <+> ppr ty_expected ]
739 ; go ty_actual ty_expected }
740 where
741 go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
742 | Just ty_e' <- tcView ty_e = go ty_a ty_e'
743
744 go (TyVarTy tv_a) ty_e
745 = do { lookup_res <- lookupTcTyVar tv_a
746 ; case lookup_res of
747 Filled ty_a' ->
748 do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:"
749 (ppr tv_a <+> text "-->" <+> ppr ty_a')
750 ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
751 Unfilled _ -> unify }
752
753 -- Historical note (Sept 16): there was a case here for
754 -- go ty_a (TyVarTy alpha)
755 -- which, in the impredicative case unified alpha := ty_a
756 -- where th_a is a polytype. Not only is this probably bogus (we
757 -- simply do not have decent story for imprdicative types), but it
758 -- caused Trac #12616 because (also bizarrely) 'deriving' code had
759 -- -XImpredicativeTypes on. I deleted the entire case.
760
761 go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
762 | not (isPredTy act_arg)
763 , not (isPredTy exp_arg)
764 = -- See Note [Co/contra-variance of subsumption checking]
765 do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
766 ; arg_wrap <- tc_sub_tc_type eq_orig given_orig ctxt exp_arg act_arg
767 ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
768 -- arg_wrap :: exp_arg ~> act_arg
769 -- res_wrap :: act-res ~> exp_res
770 where
771 given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
772 doc = text "When checking that" <+> quotes (ppr ty_actual) <+>
773 text "is more polymorphic than" <+> quotes (ppr ty_expected)
774
775 go ty_a ty_e
776 | let (tvs, theta, _) = tcSplitSigmaTy ty_a
777 , not (null tvs && null theta)
778 = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
779 ; body_wrap <- tc_sub_type_ds
780 (eq_orig { uo_actual = in_rho
781 , uo_expected = ty_expected })
782 inst_orig ctxt in_rho ty_e
783 ; return (body_wrap <.> in_wrap) }
784
785 | otherwise -- Revert to unification
786 = inst_and_unify
787 -- It's still possible that ty_actual has nested foralls. Instantiate
788 -- these, as there's no way unification will succeed with them in.
789 -- See typecheck/should_compile/T11305 for an example of when this
790 -- is important. The problem is that we're checking something like
791 -- a -> forall b. b -> b <= alpha beta gamma
792 -- where we end up with alpha := (->)
793
794 inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
795
796 -- if we haven't recurred through an arrow, then
797 -- the eq_orig will list ty_actual. In this case,
798 -- we want to update the origin to reflect the
799 -- instantiation. If we *have* recurred through
800 -- an arrow, it's better not to update.
801 ; let eq_orig' = case eq_orig of
802 TypeEqOrigin { uo_actual = orig_ty_actual }
803 | orig_ty_actual `tcEqType` ty_actual
804 , not (isIdHsWrapper wrap)
805 -> eq_orig { uo_actual = rho_a }
806 _ -> eq_orig
807
808 ; cow <- uType TypeLevel eq_orig' rho_a ty_expected
809 ; return (mkWpCastN cow <.> wrap) }
810
811
812 -- use versions without synonyms expanded
813 unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected
814
815 -----------------
816 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
817 -- expressions
818 tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
819 -> TcM (HsExpr GhcTcId)
820 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
821
822 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
823 -- convenient.
824 tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
825 -> TcM (HsExpr GhcTcId)
826 tcWrapResultO orig rn_expr expr actual_ty res_ty
827 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
828 , text "Expected:" <+> ppr res_ty ])
829 ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
830 (Just rn_expr) actual_ty res_ty
831 ; return (mkHsWrap cow expr) }
832
833 -----------------------------------
834 wrapFunResCoercion
835 :: [TcType] -- Type of args
836 -> HsWrapper -- HsExpr a -> HsExpr b
837 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
838 wrapFunResCoercion arg_tys co_fn_res
839 | isIdHsWrapper co_fn_res
840 = return idHsWrapper
841 | null arg_tys
842 = return co_fn_res
843 | otherwise
844 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
845 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
846
847
848 {- **********************************************************************
849 %* *
850 ExpType functions: tcInfer, fillInferResult
851 %* *
852 %********************************************************************* -}
853
854 -- | Infer a type using a fresh ExpType
855 -- See also Note [ExpType] in TcMType
856 -- Does not attempt to instantiate the inferred type
857 tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
858 tcInferNoInst = tcInfer False
859
860 tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
861 tcInferInst = tcInfer True
862
863 tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
864 tcInfer instantiate tc_check
865 = do { res_ty <- newInferExpType instantiate
866 ; result <- tc_check res_ty
867 ; res_ty <- readExpType res_ty
868 ; return (result, res_ty) }
869
870 fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
871 -- If wrap = fillInferResult_Inst t1 t2
872 -- => wrap :: t1 ~> t2
873 -- See Note [Deep instantiation of InferResult]
874 fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me })
875 | instantiate_me
876 = do { (wrap, rho) <- deeplyInstantiate orig ty
877 ; co <- fillInferResult rho inf_res
878 ; return (mkWpCastN co <.> wrap) }
879
880 | otherwise
881 = do { co <- fillInferResult ty inf_res
882 ; return (mkWpCastN co) }
883
884 fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
885 -- If wrap = fillInferResult t1 t2
886 -- => wrap :: t1 ~> t2
887 fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
888 , ir_ref = ref })
889 = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
890
891 ; traceTc "Filling ExpType" $
892 ppr u <+> text ":=" <+> ppr ty_to_fill_with
893
894 ; when debugIsOn (check_hole ty_to_fill_with)
895
896 ; writeTcRef ref (Just ty_to_fill_with)
897
898 ; return ty_co }
899 where
900 check_hole ty -- Debug check only
901 = do { let ty_lvl = tcTypeLevel ty
902 ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
903 ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
904 ppr ty <+> ppr (typeKind ty) $$ ppr orig_ty )
905 ; cts <- readTcRef ref
906 ; case cts of
907 Just already_there -> pprPanic "writeExpType"
908 (vcat [ ppr u
909 , ppr ty
910 , ppr already_there ])
911 Nothing -> return () }
912
913 {- Note [Deep instantiation of InferResult]
914 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
915 In some cases we want to deeply instantiate before filling in
916 an InferResult, and in some cases not. That's why InferReult
917 has the ir_inst flag.
918
919 * ir_inst = True: deeply instantiate
920
921 Consider
922 f x = (*)
923 We want to instantiate the type of (*) before returning, else we
924 will infer the type
925 f :: forall {a}. a -> forall b. Num b => b -> b -> b
926 This is surely confusing for users.
927
928 And worse, the the monomorphism restriction won't properly. The MR is
929 dealt with in simplifyInfer, and simplifyInfer has no way of
930 instantiating. This could perhaps be worked around, but it may be
931 hard to know even when instantiation should happen.
932
933 Another reason. Consider
934 f :: (?x :: Int) => a -> a
935 g y = let ?x = 3::Int in f
936 Here want to instantiate f's type so that the ?x::Int constraint
937 gets discharged by the enclosing implicit-parameter binding.
938
939 * ir_inst = False: do not instantiate
940
941 Consider this (which uses visible type application):
942
943 (let { f :: forall a. a -> a; f x = x } in f) @Int
944
945 We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
946 And we don't want to instantite the type of 'f' when we reach it,
947 else the outer visible type application won't work
948 -}
949
950 {- *********************************************************************
951 * *
952 Promoting types
953 * *
954 ********************************************************************* -}
955
956 promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
957 -- See Note [Promoting a type]
958 -- promoteTcType level ty = (co, ty')
959 -- * Returns ty' whose max level is just 'level'
960 -- and whose kind is ~# to the kind of 'ty'
961 -- and whose kind has form TYPE rr
962 -- * and co :: ty ~ ty'
963 -- * and emits constraints to justify the coercion
964 promoteTcType dest_lvl ty
965 = do { cur_lvl <- getTcLevel
966 ; if (cur_lvl `sameDepthAs` dest_lvl)
967 then dont_promote_it
968 else promote_it }
969 where
970 promote_it :: TcM (TcCoercion, TcType)
971 promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
972 -- where alpha and rr are fresh and from level dest_lvl
973 = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
974 ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
975 ; let eq_orig = TypeEqOrigin { uo_actual = ty
976 , uo_expected = prom_ty
977 , uo_thing = Nothing
978 , uo_visible = False }
979
980 ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
981 ; return (co, prom_ty) }
982
983 dont_promote_it :: TcM (TcCoercion, TcType)
984 dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
985 = do { res_kind <- newOpenTypeKind
986 ; let ty_kind = typeKind ty
987 kind_orig = TypeEqOrigin { uo_actual = ty_kind
988 , uo_expected = res_kind
989 , uo_thing = Nothing
990 , uo_visible = False }
991 ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
992 ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
993 ; return (co, ty `mkCastTy` ki_co) }
994
995 {- Note [Promoting a type]
996 ~~~~~~~~~~~~~~~~~~~~~~~~~~
997 Consider (Trac #12427)
998
999 data T where
1000 MkT :: (Int -> Int) -> a -> T
1001
1002 h y = case y of MkT v w -> v
1003
1004 We'll infer the RHS type with an expected type ExpType of
1005 (IR { ir_lvl = l, ir_ref = ref, ... )
1006 where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
1007 match will increase the level, so we'll end up in tcSubType, trying to
1008 unify the type of v,
1009 v :: Int -> Int
1010 with the expected type. But this attempt takes place at level (l+1),
1011 rightly so, since v's type could have mentioned existential variables,
1012 (like w's does) and we want to catch that.
1013
1014 So we
1015 - create a new meta-var alpha[l+1]
1016 - fill in the InferRes ref cell 'ref' with alpha
1017 - emit an equality constraint, thus
1018 [W] alpha[l+1] ~ (Int -> Int)
1019
1020 That constraint will float outwards, as it should, unless v's
1021 type mentions a skolem-captured variable.
1022
1023 This approach fails if v has a higher rank type; see
1024 Note [Promotion and higher rank types]
1025
1026
1027 Note [Promotion and higher rank types]
1028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1029 If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
1030 then we'd emit an equality
1031 [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
1032 which will sadly fail because we can't unify a unification variable
1033 with a polytype. But there is nothing really wrong with the program
1034 here.
1035
1036 We could just about solve this by "promote the type" of v, to expose
1037 its polymorphic "shape" while still leaving constraints that will
1038 prevent existential escape. But we must be careful! Exposing
1039 the "shape" of the type is precisely what we must NOT do under
1040 a GADT pattern match! So in this case we might promote the type
1041 to
1042 (forall a. a->a) -> alpha[l+1]
1043 and emit the constraint
1044 [W] alpha[l+1] ~ Int
1045 Now the poromoted type can fill the ref cell, while the emitted
1046 equality can float or not, according to the usual rules.
1047
1048 But that's not quite right! We are exposing the arrow! We could
1049 deal with that too:
1050 (forall a. mu[l+1] a a) -> alpha[l+1]
1051 with constraints
1052 [W] alpha[l+1] ~ Int
1053 [W] mu[l+1] ~ (->)
1054 Here we abstract over the '->' inside the forall, in case that
1055 is subject to an equality constraint from a GADT match.
1056
1057 Note that we kept the outer (->) because that's part of
1058 the polymorphic "shape". And becauuse of impredicativity,
1059 GADT matches can't give equalities that affect polymorphic
1060 shape.
1061
1062 This reasoning just seems too complicated, so I decided not
1063 to do it. These higher-rank notes are just here to record
1064 the thinking.
1065 -}
1066
1067 {- *********************************************************************
1068 * *
1069 Generalisation
1070 * *
1071 ********************************************************************* -}
1072
1073 -- | Take an "expected type" and strip off quantifiers to expose the
1074 -- type underneath, binding the new skolems for the @thing_inside@.
1075 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
1076 tcSkolemise :: UserTypeCtxt -> TcSigmaType
1077 -> ([TcTyVar] -> TcType -> TcM result)
1078 -- ^ These are only ever used for scoped type variables.
1079 -> TcM (HsWrapper, result)
1080 -- ^ The expression has type: spec_ty -> expected_ty
1081
1082 tcSkolemise ctxt expected_ty thing_inside
1083 -- We expect expected_ty to be a forall-type
1084 -- If not, the call is a no-op
1085 = do { traceTc "tcSkolemise" Outputable.empty
1086 ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty
1087
1088 ; lvl <- getTcLevel
1089 ; when debugIsOn $
1090 traceTc "tcSkolemise" $ vcat [
1091 ppr lvl,
1092 text "expected_ty" <+> ppr expected_ty,
1093 text "inst tyvars" <+> ppr tv_prs,
1094 text "given" <+> ppr given,
1095 text "inst type" <+> ppr rho' ]
1096
1097 -- Generally we must check that the "forall_tvs" havn't been constrained
1098 -- The interesting bit here is that we must include the free variables
1099 -- of the expected_ty. Here's an example:
1100 -- runST (newVar True)
1101 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
1102 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
1103 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
1104 -- So now s' isn't unconstrained because it's linked to a.
1105 --
1106 -- However [Oct 10] now that the untouchables are a range of
1107 -- TcTyVars, all this is handled automatically with no need for
1108 -- extra faffing around
1109
1110 ; let tvs' = map snd tv_prs
1111 skol_info = SigSkol ctxt expected_ty tv_prs
1112
1113 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
1114 thing_inside tvs' rho'
1115
1116 ; return (wrap <.> mkWpLet ev_binds, result) }
1117 -- The ev_binds returned by checkConstraints is very
1118 -- often empty, in which case mkWpLet is a no-op
1119
1120 -- | Variant of 'tcSkolemise' that takes an ExpType
1121 tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
1122 -> (ExpRhoType -> TcM result)
1123 -> TcM (HsWrapper, result)
1124 tcSkolemiseET _ et@(Infer {}) thing_inside
1125 = (idHsWrapper, ) <$> thing_inside et
1126 tcSkolemiseET ctxt (Check ty) thing_inside
1127 = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType
1128
1129 checkConstraints :: SkolemInfo
1130 -> [TcTyVar] -- Skolems
1131 -> [EvVar] -- Given
1132 -> TcM result
1133 -> TcM (TcEvBinds, result)
1134
1135 checkConstraints skol_info skol_tvs given thing_inside
1136 = do { (implics, ev_binds, result)
1137 <- buildImplication skol_info skol_tvs given thing_inside
1138 ; emitImplications implics
1139 ; return (ev_binds, result) }
1140
1141 buildImplication :: SkolemInfo
1142 -> [TcTyVar] -- Skolems
1143 -> [EvVar] -- Given
1144 -> TcM result
1145 -> TcM (Bag Implication, TcEvBinds, result)
1146 buildImplication skol_info skol_tvs given thing_inside
1147 = do { implication_needed <- implicationNeeded skol_tvs given
1148
1149 ; if implication_needed
1150 then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
1151 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
1152 ; return (implics, ev_binds, result) }
1153
1154 else -- Fast path. We check every function argument with
1155 -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
1156 -- So tihs fast path is well-exercised
1157 do { res <- thing_inside
1158 ; return (emptyBag, emptyTcEvBinds, res) } }
1159
1160 implicationNeeded :: [TcTyVar] -> [EvVar] -> TcM Bool
1161 -- With the solver producing unlifted equalities, we need
1162 -- to have an EvBindsVar for them when they might be deferred to
1163 -- runtime. Otherwise, they end up as top-level unlifted bindings,
1164 -- which are verboten. See also Note [Deferred errors for coercion holes]
1165 -- in TcErrors. cf Trac #14149 for an exmample of what goes wrong.
1166 implicationNeeded skol_tvs given
1167 | null skol_tvs
1168 , null given
1169 = -- Empty skolems and givens
1170 do { tc_lvl <- getTcLevel
1171 ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
1172 then return False -- already inside an implication
1173 else
1174 do { dflags <- getDynFlags -- If any deferral can happen,
1175 -- we must build an implication
1176 ; return (gopt Opt_DeferTypeErrors dflags ||
1177 gopt Opt_DeferTypedHoles dflags ||
1178 gopt Opt_DeferOutOfScopeVariables dflags) } }
1179
1180 | otherwise -- Non-empty skolems or givens
1181 = return True -- Definitely need an implication
1182
1183 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
1184 -> [EvVar] -> WantedConstraints
1185 -> TcM (Bag Implication, TcEvBinds)
1186 buildImplicationFor tclvl skol_info skol_tvs given wanted
1187 | isEmptyWC wanted && null given
1188 -- Optimisation : if there are no wanteds, and no givens
1189 -- don't generate an implication at all.
1190 -- Reason for the (null given): we don't want to lose
1191 -- the "inaccessible alternative" error check
1192 = return (emptyBag, emptyTcEvBinds)
1193
1194 | otherwise
1195 = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
1196 do { ev_binds_var <- newTcEvBinds
1197 ; env <- getLclEnv
1198 ; let implic = Implic { ic_tclvl = tclvl
1199 , ic_skols = skol_tvs
1200 , ic_no_eqs = False
1201 , ic_given = given
1202 , ic_wanted = wanted
1203 , ic_status = IC_Unsolved
1204 , ic_binds = ev_binds_var
1205 , ic_env = env
1206 , ic_needed = emptyVarSet
1207 , ic_info = skol_info }
1208
1209 ; return (unitBag implic, TcEvBinds ev_binds_var) }
1210
1211 {-
1212 ************************************************************************
1213 * *
1214 Boxy unification
1215 * *
1216 ************************************************************************
1217
1218 The exported functions are all defined as versions of some
1219 non-exported generic functions.
1220 -}
1221
1222 unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1'
1223 -> TcTauType -> TcTauType -> TcM TcCoercionN
1224 -- Actual and expected types
1225 -- Returns a coercion : ty1 ~ ty2
1226 unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
1227 uType TypeLevel origin ty1 ty2
1228 where
1229 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
1230 , uo_thing = ppr <$> thing
1231 , uo_visible = True } -- always called from a visible context
1232
1233 unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
1234 unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
1235 uType KindLevel origin ty1 ty2
1236 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
1237 , uo_thing = ppr <$> thing
1238 , uo_visible = True } -- also always from a visible context
1239
1240 ---------------
1241 unifyPred :: PredType -> PredType -> TcM TcCoercionN
1242 -- Actual and expected types
1243 unifyPred = unifyType Nothing
1244
1245 ---------------
1246 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
1247 -- Actual and expected types
1248 unifyTheta theta1 theta2
1249 = do { checkTc (equalLength theta1 theta2)
1250 (vcat [text "Contexts differ in length",
1251 nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"])
1252 ; zipWithM unifyPred theta1 theta2 }
1253
1254 {-
1255 %************************************************************************
1256 %* *
1257 uType and friends
1258 %* *
1259 %************************************************************************
1260
1261 uType is the heart of the unifier.
1262 -}
1263
1264 uType, uType_defer
1265 :: TypeOrKind
1266 -> CtOrigin
1267 -> TcType -- ty1 is the *actual* type
1268 -> TcType -- ty2 is the *expected* type
1269 -> TcM Coercion
1270
1271 --------------
1272 -- It is always safe to defer unification to the main constraint solver
1273 -- See Note [Deferred unification]
1274 uType_defer t_or_k origin ty1 ty2
1275 = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
1276
1277 -- Error trace only
1278 -- NB. do *not* call mkErrInfo unless tracing is on,
1279 -- because it is hugely expensive (#5631)
1280 ; whenDOptM Opt_D_dump_tc_trace $ do
1281 { ctxt <- getErrCtxt
1282 ; doc <- mkErrInfo emptyTidyEnv ctxt
1283 ; traceTc "utype_defer" (vcat [ debugPprType ty1
1284 , debugPprType ty2
1285 , pprCtOrigin origin
1286 , doc])
1287 ; traceTc "utype_defer2" (ppr co)
1288 }
1289 ; return co }
1290
1291 --------------
1292 uType t_or_k origin orig_ty1 orig_ty2
1293 = do { tclvl <- getTcLevel
1294 ; traceTc "u_tys" $ vcat
1295 [ text "tclvl" <+> ppr tclvl
1296 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
1297 , pprCtOrigin origin]
1298 ; co <- go orig_ty1 orig_ty2
1299 ; if isReflCo co
1300 then traceTc "u_tys yields no coercion" Outputable.empty
1301 else traceTc "u_tys yields coercion:" (ppr co)
1302 ; return co }
1303 where
1304 go :: TcType -> TcType -> TcM Coercion
1305 -- The arguments to 'go' are always semantically identical
1306 -- to orig_ty{1,2} except for looking through type synonyms
1307
1308 -- Variables; go for uVar
1309 -- Note that we pass in *original* (before synonym expansion),
1310 -- so that type variables tend to get filled in with
1311 -- the most informative version of the type
1312 go (TyVarTy tv1) ty2
1313 = do { lookup_res <- lookupTcTyVar tv1
1314 ; case lookup_res of
1315 Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
1316 ; go ty1 ty2 }
1317 Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
1318 go ty1 (TyVarTy tv2)
1319 = do { lookup_res <- lookupTcTyVar tv2
1320 ; case lookup_res of
1321 Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
1322 ; go ty1 ty2 }
1323 Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
1324
1325 -- See Note [Expanding synonyms during unification]
1326 go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
1327 | tc1 == tc2
1328 = return $ mkReflCo Nominal ty1
1329
1330 -- See Note [Expanding synonyms during unification]
1331 --
1332 -- Also NB that we recurse to 'go' so that we don't push a
1333 -- new item on the origin stack. As a result if we have
1334 -- type Foo = Int
1335 -- and we try to unify Foo ~ Bool
1336 -- we'll end up saying "can't match Foo with Bool"
1337 -- rather than "can't match "Int with Bool". See Trac #4535.
1338 go ty1 ty2
1339 | Just ty1' <- tcView ty1 = go ty1' ty2
1340 | Just ty2' <- tcView ty2 = go ty1 ty2'
1341
1342 go (CastTy t1 co1) t2
1343 = do { co_tys <- go t1 t2
1344 ; return (mkCoherenceLeftCo co_tys co1) }
1345
1346 go t1 (CastTy t2 co2)
1347 = do { co_tys <- go t1 t2
1348 ; return (mkCoherenceRightCo co_tys co2) }
1349
1350 -- Functions (or predicate functions) just check the two parts
1351 go (FunTy fun1 arg1) (FunTy fun2 arg2)
1352 = do { co_l <- uType t_or_k origin fun1 fun2
1353 ; co_r <- uType t_or_k origin arg1 arg2
1354 ; return $ mkFunCo Nominal co_l co_r }
1355
1356 -- Always defer if a type synonym family (type function)
1357 -- is involved. (Data families behave rigidly.)
1358 go ty1@(TyConApp tc1 _) ty2
1359 | isTypeFamilyTyCon tc1 = defer ty1 ty2
1360 go ty1 ty2@(TyConApp tc2 _)
1361 | isTypeFamilyTyCon tc2 = defer ty1 ty2
1362
1363 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1364 -- See Note [Mismatched type lists and application decomposition]
1365 | tc1 == tc2, equalLength tys1 tys2
1366 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
1367 do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
1368 ; return $ mkTyConAppCo Nominal tc1 cos }
1369 where
1370 origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
1371 (tcTyConVisibilities tc1)
1372
1373 go (LitTy m) ty@(LitTy n)
1374 | m == n
1375 = return $ mkNomReflCo ty
1376
1377 -- See Note [Care with type applications]
1378 -- Do not decompose FunTy against App;
1379 -- it's often a type error, so leave it for the constraint solver
1380 go (AppTy s1 t1) (AppTy s2 t2)
1381 = go_app (isNextArgVisible s1) s1 t1 s2 t2
1382
1383 go (AppTy s1 t1) (TyConApp tc2 ts2)
1384 | Just (ts2', t2') <- snocView ts2
1385 = ASSERT( mightBeUnsaturatedTyCon tc2 )
1386 go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
1387
1388 go (TyConApp tc1 ts1) (AppTy s2 t2)
1389 | Just (ts1', t1') <- snocView ts1
1390 = ASSERT( mightBeUnsaturatedTyCon tc1 )
1391 go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
1392
1393 go (CoercionTy co1) (CoercionTy co2)
1394 = do { let ty1 = coercionType co1
1395 ty2 = coercionType co2
1396 ; kco <- uType KindLevel
1397 (KindEqOrigin orig_ty1 (Just orig_ty2) origin
1398 (Just t_or_k))
1399 ty1 ty2
1400 ; return $ mkProofIrrelCo Nominal kco co1 co2 }
1401
1402 -- Anything else fails
1403 -- E.g. unifying for-all types, which is relative unusual
1404 go ty1 ty2 = defer ty1 ty2
1405
1406 ------------------
1407 defer ty1 ty2 -- See Note [Check for equality before deferring]
1408 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
1409 | otherwise = uType_defer t_or_k origin ty1 ty2
1410
1411 ------------------
1412 go_app vis s1 t1 s2 t2
1413 = do { co_s <- uType t_or_k origin s1 s2
1414 ; let arg_origin
1415 | vis = origin
1416 | otherwise = toInvisibleOrigin origin
1417 ; co_t <- uType t_or_k arg_origin t1 t2
1418 ; return $ mkAppCo co_s co_t }
1419
1420 {- Note [Check for equality before deferring]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
1423 If ty involves a type function we may defer, which isn't very sensible.
1424 An egregious example of this was in test T9872a, which has a type signature
1425 Proxy :: Proxy (Solutions Cubes)
1426 Doing the ambiguity check on this signature generates the equality
1427 Solutions Cubes ~ Solutions Cubes
1428 and currently the constraint solver normalises both sides at vast cost.
1429 This little short-cut in 'defer' helps quite a bit.
1430
1431 Note [Care with type applications]
1432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1433 Note: type applications need a bit of care!
1434 They can match FunTy and TyConApp, so use splitAppTy_maybe
1435 NB: we've already dealt with type variables and Notes,
1436 so if one type is an App the other one jolly well better be too
1437
1438 Note [Mismatched type lists and application decomposition]
1439 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1440 When we find two TyConApps, you might think that the argument lists
1441 are guaranteed equal length. But they aren't. Consider matching
1442 w (T x) ~ Foo (T x y)
1443 We do match (w ~ Foo) first, but in some circumstances we simply create
1444 a deferred constraint; and then go ahead and match (T x ~ T x y).
1445 This came up in Trac #3950.
1446
1447 So either
1448 (a) either we must check for identical argument kinds
1449 when decomposing applications,
1450
1451 (b) or we must be prepared for ill-kinded unification sub-problems
1452
1453 Currently we adopt (b) since it seems more robust -- no need to maintain
1454 a global invariant.
1455
1456 Note [Expanding synonyms during unification]
1457 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1458 We expand synonyms during unification, but:
1459 * We expand *after* the variable case so that we tend to unify
1460 variables with un-expanded type synonym. This just makes it
1461 more likely that the inferred types will mention type synonyms
1462 understandable to the user
1463
1464 * We expand *before* the TyConApp case. For example, if we have
1465 type Phantom a = Int
1466 and are unifying
1467 Phantom Int ~ Phantom Char
1468 it is *wrong* to unify Int and Char.
1469
1470 * The problem case immediately above can happen only with arguments
1471 to the tycon. So we check for nullary tycons *before* expanding.
1472 This is particularly helpful when checking (* ~ *), because * is
1473 now a type synonym.
1474
1475 Note [Deferred Unification]
1476 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1477 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
1478 and yet its consistency is undetermined. Previously, there was no way to still
1479 make it consistent. So a mismatch error was issued.
1480
1481 Now these unifications are deferred until constraint simplification, where type
1482 family instances and given equations may (or may not) establish the consistency.
1483 Deferred unifications are of the form
1484 F ... ~ ...
1485 or x ~ ...
1486 where F is a type function and x is a type variable.
1487 E.g.
1488 id :: x ~ y => x -> y
1489 id e = e
1490
1491 involves the unification x = y. It is deferred until we bring into account the
1492 context x ~ y to establish that it holds.
1493
1494 If available, we defer original types (rather than those where closed type
1495 synonyms have already been expanded via tcCoreView). This is, as usual, to
1496 improve error messages.
1497
1498
1499 ************************************************************************
1500 * *
1501 uVar and friends
1502 * *
1503 ************************************************************************
1504
1505 @uVar@ is called when at least one of the types being unified is a
1506 variable. It does {\em not} assume that the variable is a fixed point
1507 of the substitution; rather, notice that @uVar@ (defined below) nips
1508 back into @uTys@ if it turns out that the variable is already bound.
1509 -}
1510
1511 ----------
1512 uUnfilledVar :: CtOrigin
1513 -> TypeOrKind
1514 -> SwapFlag
1515 -> TcTyVar -- Tyvar 1
1516 -> TcTauType -- Type 2
1517 -> TcM Coercion
1518 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
1519 -- It might be a skolem, or untouchable, or meta
1520
1521 uUnfilledVar origin t_or_k swapped tv1 ty2
1522 = do { ty2 <- zonkTcType ty2
1523 -- Zonk to expose things to the
1524 -- occurs check, and so that if ty2
1525 -- looks like a type variable then it
1526 -- /is/ a type variable
1527 ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
1528
1529 ----------
1530 uUnfilledVar1 :: CtOrigin
1531 -> TypeOrKind
1532 -> SwapFlag
1533 -> TcTyVar -- Tyvar 1
1534 -> TcTauType -- Type 2, zonked
1535 -> TcM Coercion
1536 uUnfilledVar1 origin t_or_k swapped tv1 ty2
1537 | Just tv2 <- tcGetTyVar_maybe ty2
1538 = go tv2
1539
1540 | otherwise
1541 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1542
1543 where
1544 -- 'go' handles the case where both are
1545 -- tyvars so we might want to swap
1546 go tv2 | tv1 == tv2 -- Same type variable => no-op
1547 = return (mkNomReflCo (mkTyVarTy tv1))
1548
1549 | swapOverTyVars tv1 tv2 -- Distinct type variables
1550 = uUnfilledVar2 origin t_or_k (flipSwap swapped)
1551 tv2 (mkTyVarTy tv1)
1552
1553 | otherwise
1554 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1555
1556 ----------
1557 uUnfilledVar2 :: CtOrigin
1558 -> TypeOrKind
1559 -> SwapFlag
1560 -> TcTyVar -- Tyvar 1
1561 -> TcTauType -- Type 2, zonked
1562 -> TcM Coercion
1563 uUnfilledVar2 origin t_or_k swapped tv1 ty2
1564 = do { dflags <- getDynFlags
1565 ; cur_lvl <- getTcLevel
1566 ; go dflags cur_lvl }
1567 where
1568 go dflags cur_lvl
1569 | canSolveByUnification cur_lvl tv1 ty2
1570 , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
1571 = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
1572 ; if isTcReflCo co_k -- only proceed if the kinds matched.
1573
1574 then do { writeMetaTyVar tv1 ty2'
1575 ; return (mkTcNomReflCo ty2') }
1576 else defer } -- this cannot be solved now.
1577 -- See Note [Equalities with incompatible kinds]
1578 -- in TcCanonical
1579
1580 | otherwise
1581 = defer
1582 -- Occurs check or an untouchable: just defer
1583 -- NB: occurs check isn't necessarily fatal:
1584 -- eg tv1 occured in type family parameter
1585
1586 ty1 = mkTyVarTy tv1
1587 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
1588
1589 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
1590
1591 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
1592 swapOverTyVars tv1 tv2
1593 | isFmvTyVar tv1 = False -- See Note [Fmv Orientation Invariant]
1594 | isFmvTyVar tv2 = True
1595
1596 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1597 -- If tv1 is touchable, swap only if tv2 is also
1598 -- touchable and it's strictly better to update the latter
1599 -- But see Note [Avoid unnecessary swaps]
1600 = case metaTyVarTcLevel_maybe tv2 of
1601 Nothing -> False
1602 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1603 | lvl1 `strictlyDeeperThan` lvl2 -> False
1604 | otherwise -> nicer_to_update tv2
1605
1606 -- So tv1 is not a meta tyvar
1607 -- If only one is a meta tyvar, put it on the left
1608 -- This is not because it'll be solved; but because
1609 -- the floating step looks for meta tyvars on the left
1610 | isMetaTyVar tv2 = True
1611
1612 -- So neither is a meta tyvar (including FlatMetaTv)
1613
1614 -- If only one is a flatten skolem, put it on the left
1615 -- See Note [Eliminate flat-skols]
1616 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1617
1618 | otherwise = False
1619
1620 where
1621 nicer_to_update tv2
1622 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1623 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1624
1625 -- @trySpontaneousSolve wi@ solves equalities where one side is a
1626 -- touchable unification variable.
1627 -- Returns True <=> spontaneous solve happened
1628 canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
1629 canSolveByUnification tclvl tv xi
1630 | isTouchableMetaTyVar tclvl tv
1631 = case metaTyVarInfo tv of
1632 SigTv -> is_tyvar xi
1633 _ -> True
1634
1635 | otherwise -- Untouchable
1636 = False
1637 where
1638 is_tyvar xi
1639 = case tcGetTyVar_maybe xi of
1640 Nothing -> False
1641 Just tv -> case tcTyVarDetails tv of
1642 MetaTv { mtv_info = info }
1643 -> case info of
1644 SigTv -> True
1645 _ -> False
1646 SkolemTv {} -> True
1647 RuntimeUnk -> True
1648
1649 {- Note [Fmv Orientation Invariant]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 * We always orient a constraint
1652 fmv ~ alpha
1653 with fmv on the left, even if alpha is
1654 a touchable unification variable
1655
1656 Reason: doing it the other way round would unify alpha:=fmv, but that
1657 really doesn't add any info to alpha. But a later constraint alpha ~
1658 Int might unlock everything. Comment:9 of #12526 gives a detailed
1659 example.
1660
1661 WARNING: I've gone to and fro on this one several times.
1662 I'm now pretty sure that unifying alpha:=fmv is a bad idea!
1663 So orienting with fmvs on the left is a good thing.
1664
1665 This example comes from IndTypesPerfMerge. (Others include
1666 T10226, T10009.)
1667 From the ambiguity check for
1668 f :: (F a ~ a) => a
1669 we get:
1670 [G] F a ~ a
1671 [WD] F alpha ~ alpha, alpha ~ a
1672
1673 From Givens we get
1674 [G] F a ~ fsk, fsk ~ a
1675
1676 Now if we flatten we get
1677 [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
1678
1679 Now, if we unified alpha := fmv, we'd get
1680 [WD] F fmv ~ fmv, [WD] fmv ~ a
1681 And now we are stuck.
1682
1683 So instead the Fmv Orientation Invariant puts te fmv on the
1684 left, giving
1685 [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
1686
1687 Now we get alpha:=a, and everything works out
1688
1689 Note [Prevent unification with type families]
1690 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1691 We prevent unification with type families because of an uneasy compromise.
1692 It's perfectly sound to unify with type families, and it even improves the
1693 error messages in the testsuite. It also modestly improves performance, at
1694 least in some cases. But it's disastrous for test case perf/compiler/T3064.
1695 Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
1696 What do we do? Do we reduce F? Or do we use the given? Hard to know what's
1697 best. GHC reduces. This is a disaster for T3064, where the type's size
1698 spirals out of control during reduction. (We're not helped by the fact that
1699 the flattener re-flattens all the arguments every time around.) If we prevent
1700 unification with type families, then the solver happens to use the equality
1701 before expanding the type family.
1702
1703 It would be lovely in the future to revisit this problem and remove this
1704 extra, unnecessary check. But we retain it for now as it seems to work
1705 better in practice.
1706
1707 Note [Refactoring hazard: checkTauTvUpdate]
1708 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1709 I (Richard E.) have a sad story about refactoring this code, retained here
1710 to prevent others (or a future me!) from falling into the same traps.
1711
1712 It all started with #11407, which was caused by the fact that the TyVarTy
1713 case of defer_me didn't look in the kind. But it seemed reasonable to
1714 simply remove the defer_me check instead.
1715
1716 It referred to two Notes (since removed) that were out of date, and the
1717 fast_check code in occurCheckExpand seemed to do just about the same thing as
1718 defer_me. The one piece that defer_me did that wasn't repeated by
1719 occurCheckExpand was the type-family check. (See Note [Prevent unification
1720 with type families].) So I checked the result of occurCheckExpand for any
1721 type family occurrences and deferred if there were any. This was done
1722 in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
1723
1724 This approach turned out not to be performant, because the expanded
1725 type was bigger than the original type, and tyConsOfType (needed to
1726 see if there are any type family occurrences) looks through type
1727 synonyms. So it then struck me that we could dispense with the
1728 defer_me check entirely. This simplified the code nicely, and it cut
1729 the allocations in T5030 by half. But, as documented in Note [Prevent
1730 unification with type families], this destroyed performance in
1731 T3064. Regardless, I missed this regression and the change was
1732 committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
1733
1734 Bottom lines:
1735 * defer_me is back, but now fixed w.r.t. #11407.
1736 * Tread carefully before you start to refactor here. There can be
1737 lots of hard-to-predict consequences.
1738
1739 Note [Type synonyms and the occur check]
1740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1741 Generally speaking we try to update a variable with type synonyms not
1742 expanded, which improves later error messages, unless looking
1743 inside a type synonym may help resolve a spurious occurs check
1744 error. Consider:
1745 type A a = ()
1746
1747 f :: (A a -> a -> ()) -> ()
1748 f = \ _ -> ()
1749
1750 x :: ()
1751 x = f (\ x p -> p x)
1752
1753 We will eventually get a constraint of the form t ~ A t. The ok function above will
1754 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1755 unified with the original type A t, we would lead the type checker into an infinite loop.
1756
1757 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1758 the ok function expands the synonym to detect opportunities for occurs check success using
1759 the underlying definition of the type synonym.
1760
1761 The same applies later on in the constraint interaction code; see TcInteract,
1762 function @occ_check_ok@.
1763
1764 Note [Non-TcTyVars in TcUnify]
1765 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1766 Because the same code is now shared between unifying types and unifying
1767 kinds, we sometimes will see proper TyVars floating around the unifier.
1768 Example (from test case polykinds/PolyKinds12):
1769
1770 type family Apply (f :: k1 -> k2) (x :: k1) :: k2
1771 type instance Apply g y = g y
1772
1773 When checking the instance declaration, we first *kind-check* the LHS
1774 and RHS, discovering that the instance really should be
1775
1776 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
1777
1778 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
1779 as a second pass, we desugar the RHS (which is done in functions prefixed
1780 with "tc" in TcTyClsDecls"). By this time, all the kind-vars are proper
1781 TyVars, not TcTyVars, get some kind unification must happen.
1782
1783 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
1784 meta-tyvar.
1785
1786 This used to not be necessary for type-checking (that is, before * :: *)
1787 because expressions get desugared via an algorithm separate from
1788 type-checking (with wrappers, etc.). Types get desugared very differently,
1789 causing this wibble in behavior seen here.
1790 -}
1791
1792 data LookupTyVarResult -- The result of a lookupTcTyVar call
1793 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1794 | Filled TcType
1795
1796 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1797 lookupTcTyVar tyvar
1798 | MetaTv { mtv_ref = ref } <- details
1799 = do { meta_details <- readMutVar ref
1800 ; case meta_details of
1801 Indirect ty -> return (Filled ty)
1802 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1803 -- Note [Unifying untouchables]
1804 ; if is_touchable then
1805 return (Unfilled details)
1806 else
1807 return (Unfilled vanillaSkolemTv) } }
1808 | otherwise
1809 = return (Unfilled details)
1810 where
1811 details = tcTyVarDetails tyvar
1812
1813 {-
1814 Note [Unifying untouchables]
1815 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1816 We treat an untouchable type variable as if it was a skolem. That
1817 ensures it won't unify with anything. It's a slight had, because
1818 we return a made-up TcTyVarDetails, but I think it works smoothly.
1819 -}
1820
1821 -- | Breaks apart a function kind into its pieces.
1822 matchExpectedFunKind :: Outputable fun
1823 => fun -- ^ type, only for errors
1824 -> TcKind -- ^ function kind
1825 -> TcM (Coercion, TcKind, TcKind)
1826 -- ^ co :: old_kind ~ arg -> res
1827 matchExpectedFunKind hs_ty = go
1828 where
1829 go k | Just k' <- tcView k = go k'
1830
1831 go k@(TyVarTy kvar)
1832 | isTcTyVar kvar, isMetaTyVar kvar
1833 = do { maybe_kind <- readMetaTyVar kvar
1834 ; case maybe_kind of
1835 Indirect fun_kind -> go fun_kind
1836 Flexi -> defer k }
1837
1838 go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
1839 go other = defer other
1840
1841 defer k
1842 = do { arg_kind <- newMetaKindVar
1843 ; res_kind <- newMetaKindVar
1844 ; let new_fun = mkFunTy arg_kind res_kind
1845 origin = TypeEqOrigin { uo_actual = k
1846 , uo_expected = new_fun
1847 , uo_thing = Just (ppr hs_ty)
1848 , uo_visible = True
1849 }
1850 ; co <- uType KindLevel origin k new_fun
1851 ; return (co, arg_kind, res_kind) }
1852
1853
1854 {- *********************************************************************
1855 * *
1856 Occurrence checking
1857 * *
1858 ********************************************************************* -}
1859
1860
1861 {- Note [Occurs check expansion]
1862 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1863 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1864 of occurrences of tv outside type function arguments, if that is
1865 possible; otherwise, it returns Nothing.
1866
1867 For example, suppose we have
1868 type F a b = [a]
1869 Then
1870 occCheckExpand b (F Int b) = Just [Int]
1871 but
1872 occCheckExpand a (F a Int) = Nothing
1873
1874 We don't promise to do the absolute minimum amount of expanding
1875 necessary, but we try not to do expansions we don't need to. We
1876 prefer doing inner expansions first. For example,
1877 type F a b = (a, Int, a, [a])
1878 type G b = Char
1879 We have
1880 occCheckExpand b (F (G b)) = Just (F Char)
1881 even though we could also expand F to get rid of b.
1882
1883 The two variants of the function are to support TcUnify.checkTauTvUpdate,
1884 which wants to prevent unification with type families. For more on this
1885 point, see Note [Prevent unification with type families] in TcUnify.
1886
1887 Note [Occurrence checking: look inside kinds]
1888 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1889 Suppose we are considering unifying
1890 (alpha :: *) ~ Int -> (beta :: alpha -> alpha)
1891 This may be an error (what is that alpha doing inside beta's kind?),
1892 but we must not make the mistake of actuallyy unifying or we'll
1893 build an infinite data structure. So when looking for occurrences
1894 of alpha in the rhs, we must look in the kinds of type variables
1895 that occur there.
1896
1897 NB: we may be able to remove the problem via expansion; see
1898 Note [Occurs check expansion]. So we have to try that.
1899
1900 Note [Checking for foralls]
1901 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1902 Unless we have -XImpredicativeTypes (which is a totally unsupported
1903 feature), we do not want to unify
1904 alpha ~ (forall a. a->a) -> Int
1905 So we look for foralls hidden inside the type, and it's convenient
1906 to do that at the same time as the occurs check (which looks for
1907 occurrences of alpha).
1908
1909 However, it's not just a question of looking for foralls /anywhere/!
1910 Consider
1911 (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
1912 This is legal; e.g. dependent/should_compile/T11635.
1913
1914 We don't want to reject it because of the forall in beta's kind,
1915 but (see Note [Occurrence checking: look inside kinds]) we do
1916 need to look in beta's kind. So we carry a flag saying if a 'forall'
1917 is OK, and sitch the flag on when stepping inside a kind.
1918
1919 Why is it OK? Why does it not count as impredicative polymorphism?
1920 The reason foralls are bad is because we reply on "seeing" foralls
1921 when doing implicit instantiation. But the forall inside the kind is
1922 fine. We'll generate a kind equality constraint
1923 (forall k. k->*) ~ (forall k. k->*)
1924 to check that the kinds of lhs and rhs are compatible. If alpha's
1925 kind had instead been
1926 (alpha :: kappa)
1927 then this kind equality would rightly complain about unifying kappa
1928 with (forall k. k->*)
1929
1930 -}
1931
1932 data OccCheckResult a
1933 = OC_OK a
1934 | OC_Bad -- Forall or type family
1935 | OC_Occurs
1936
1937 instance Functor OccCheckResult where
1938 fmap = liftM
1939
1940 instance Applicative OccCheckResult where
1941 pure = OC_OK
1942 (<*>) = ap
1943
1944 instance Monad OccCheckResult where
1945 OC_OK x >>= k = k x
1946 OC_Bad >>= _ = OC_Bad
1947 OC_Occurs >>= _ = OC_Occurs
1948
1949 occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
1950 -- Just for error-message generation; so we return OccCheckResult
1951 -- so the caller can report the right kind of error
1952 -- Check whether
1953 -- a) the given variable occurs in the given type.
1954 -- b) there is a forall in the type (unless we have -XImpredicativeTypes)
1955 occCheckForErrors dflags tv ty
1956 = case preCheck dflags True tv ty of
1957 OC_OK _ -> OC_OK ()
1958 OC_Bad -> OC_Bad
1959 OC_Occurs -> case occCheckExpand tv ty of
1960 Nothing -> OC_Occurs
1961 Just _ -> OC_OK ()
1962
1963 ----------------
1964 metaTyVarUpdateOK :: DynFlags
1965 -> TcTyVar -- tv :: k1
1966 -> TcType -- ty :: k2
1967 -> Maybe TcType -- possibly-expanded ty
1968 -- (metaTyFVarUpdateOK tv ty)
1969 -- We are about to update the meta-tyvar tv with ty
1970 -- Check (a) that tv doesn't occur in ty (occurs check)
1971 -- (b) that ty does not have any foralls
1972 -- (in the impredicative case), or type functions
1973 --
1974 -- We have two possible outcomes:
1975 -- (1) Return the type to update the type variable with,
1976 -- [we know the update is ok]
1977 -- (2) Return Nothing,
1978 -- [the update might be dodgy]
1979 --
1980 -- Note that "Nothing" does not mean "definite error". For example
1981 -- type family F a
1982 -- type instance F Int = Int
1983 -- consider
1984 -- a ~ F a
1985 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
1986 -- we return Nothing, leaving it to the later constraint simplifier to
1987 -- sort matters out.
1988 --
1989 -- See Note [Refactoring hazard: checkTauTvUpdate]
1990
1991 metaTyVarUpdateOK dflags tv ty
1992 = case preCheck dflags False tv ty of
1993 -- False <=> type families not ok
1994 -- See Note [Prevent unification with type families]
1995 OC_OK _ -> Just ty
1996 OC_Bad -> Nothing -- forall or type function
1997 OC_Occurs -> occCheckExpand tv ty
1998
1999 preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
2000 -- A quick check for
2001 -- (a) a forall type (unless -XImpredivativeTypes)
2002 -- (b) a type family
2003 -- (c) an occurrence of the type variable (occurs check)
2004 --
2005 -- For (a) and (b) we check only the top level of the type, NOT
2006 -- inside the kinds of variables it mentions. But for (c) we do
2007 -- look in the kinds of course.
2008
2009 preCheck dflags ty_fam_ok tv ty
2010 = fast_check ty
2011 where
2012 details = tcTyVarDetails tv
2013 impredicative_ok = canUnifyWithPolyType dflags details
2014
2015 ok :: OccCheckResult ()
2016 ok = OC_OK ()
2017
2018 fast_check :: TcType -> OccCheckResult ()
2019 fast_check (TyVarTy tv')
2020 | tv == tv' = OC_Occurs
2021 | otherwise = fast_check_occ (tyVarKind tv')
2022 -- See Note [Occurrence checking: look inside kinds]
2023
2024 fast_check (TyConApp tc tys)
2025 | bad_tc tc = OC_Bad
2026 | otherwise = mapM fast_check tys >> ok
2027 fast_check (LitTy {}) = ok
2028 fast_check (FunTy a r) = fast_check a >> fast_check r
2029 fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
2030 fast_check (CastTy ty co) = fast_check ty >> fast_check_co co
2031 fast_check (CoercionTy co) = fast_check_co co
2032 fast_check (ForAllTy (TvBndr tv' _) ty)
2033 | not impredicative_ok = OC_Bad
2034 | tv == tv' = ok
2035 | otherwise = do { fast_check_occ (tyVarKind tv')
2036 ; fast_check_occ ty }
2037 -- Under a forall we look only for occurrences of
2038 -- the type variable
2039
2040 -- For kinds, we only do an occurs check; we do not worry
2041 -- about type families or foralls
2042 -- See Note [Checking for foralls]
2043 fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
2044 | otherwise = ok
2045
2046 -- For coercions, we are only doing an occurs check here;
2047 -- no bother about impredicativity in coercions, as they're
2048 -- inferred
2049 fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
2050 | otherwise = ok
2051
2052 bad_tc :: TyCon -> Bool
2053 bad_tc tc
2054 | not (impredicative_ok || isTauTyCon tc) = True
2055 | not (ty_fam_ok || isFamFreeTyCon tc) = True
2056 | otherwise = False
2057
2058 occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
2059 -- See Note [Occurs check expansion]
2060 -- We may have needed to do some type synonym unfolding in order to
2061 -- get rid of the variable (or forall), so we also return the unfolded
2062 -- version of the type, which is guaranteed to be syntactically free
2063 -- of the given type variable. If the type is already syntactically
2064 -- free of the variable, then the same type is returned.
2065 occCheckExpand tv ty
2066 = go emptyVarEnv ty
2067 where
2068 go :: VarEnv TyVar -> Type -> Maybe Type
2069 -- The VarEnv carries mappings necessary
2070 -- because of kind expansion
2071 go env (TyVarTy tv')
2072 | tv == tv' = Nothing
2073 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2074 | otherwise = do { k' <- go env (tyVarKind tv')
2075 ; return (mkTyVarTy $
2076 setTyVarKind tv' k') }
2077 -- See Note [Occurrence checking: look inside kinds]
2078
2079 go _ ty@(LitTy {}) = return ty
2080 go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
2081 ; ty2' <- go env ty2
2082 ; return (mkAppTy ty1' ty2') }
2083 go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
2084 ; ty2' <- go env ty2
2085 ; return (mkFunTy ty1' ty2') }
2086 go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
2087 | tv == tv' = return ty
2088 | otherwise = do { ki' <- go env (tyVarKind tv')
2089 ; let tv'' = setTyVarKind tv' ki'
2090 env' = extendVarEnv env tv' tv''
2091 ; body' <- go env' body_ty
2092 ; return (ForAllTy (TvBndr tv'' vis) body') }
2093
2094 -- For a type constructor application, first try expanding away the
2095 -- offending variable from the arguments. If that doesn't work, next
2096 -- see if the type constructor is a type synonym, and if so, expand
2097 -- it and try again.
2098 go env ty@(TyConApp tc tys)
2099 = case mapM (go env) tys of
2100 Just tys' -> return (mkTyConApp tc tys')
2101 Nothing | Just ty' <- tcView ty -> go env ty'
2102 | otherwise -> Nothing
2103 -- Failing that, try to expand a synonym
2104
2105 go env (CastTy ty co) = do { ty' <- go env ty
2106 ; co' <- go_co env co
2107 ; return (mkCastTy ty' co') }
2108 go env (CoercionTy co) = do { co' <- go_co env co
2109 ; return (mkCoercionTy co') }
2110
2111 ------------------
2112 go_co env (Refl r ty) = do { ty' <- go env ty
2113 ; return (mkReflCo r ty') }
2114 -- Note: Coercions do not contain type synonyms
2115 go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args
2116 ; return (mkTyConAppCo r tc args') }
2117 go_co env (AppCo co arg) = do { co' <- go_co env co
2118 ; arg' <- go_co env arg
2119 ; return (mkAppCo co' arg') }
2120 go_co env co@(ForAllCo tv' kind_co body_co)
2121 | tv == tv' = return co
2122 | otherwise = do { kind_co' <- go_co env kind_co
2123 ; let tv'' = setTyVarKind tv' $
2124 pFst (coercionKind kind_co')
2125 env' = extendVarEnv env tv' tv''
2126 ; body' <- go_co env' body_co
2127 ; return (ForAllCo tv'' kind_co' body') }
2128 go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1
2129 ; co2' <- go_co env co2
2130 ; return (mkFunCo r co1' co2') }
2131 go_co env (CoVarCo c) = do { k' <- go env (varType c)
2132 ; return (mkCoVarCo (setVarType c k')) }
2133 go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
2134 ; return (mkAxiomInstCo ax ind args') }
2135 go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p
2136 ; ty1' <- go env ty1
2137 ; ty2' <- go env ty2
2138 ; return (mkUnivCo p' r ty1' ty2') }
2139 go_co env (SymCo co) = do { co' <- go_co env co
2140 ; return (mkSymCo co') }
2141 go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
2142 ; co2' <- go_co env co2
2143 ; return (mkTransCo co1' co2') }
2144 go_co env (NthCo n co) = do { co' <- go_co env co
2145 ; return (mkNthCo n co') }
2146 go_co env (LRCo lr co) = do { co' <- go_co env co
2147 ; return (mkLRCo lr co') }
2148 go_co env (InstCo co arg) = do { co' <- go_co env co
2149 ; arg' <- go_co env arg
2150 ; return (mkInstCo co' arg') }
2151 go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1
2152 ; co2' <- go_co env co2
2153 ; return (mkCoherenceCo co1' co2') }
2154 go_co env (KindCo co) = do { co' <- go_co env co
2155 ; return (mkKindCo co') }
2156 go_co env (SubCo co) = do { co' <- go_co env co
2157 ; return (mkSubCo co') }
2158 go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs
2159 ; return (mkAxiomRuleCo ax cs') }
2160
2161 ------------------
2162 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2163 go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
2164 go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
2165 go_prov _ p@(PluginProv _) = return p
2166 go_prov _ p@(HoleProv _) = return p
2167
2168 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
2169 canUnifyWithPolyType dflags details
2170 = case details of
2171 MetaTv { mtv_info = SigTv } -> False
2172 MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags
2173 _other -> True
2174 -- We can have non-meta tyvars in given constraints