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