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