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