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