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