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