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