vectorise: Put it out of its misery
[ghc.git] / compiler / typecheck / TcUnify.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Type subsumption and unification
7 -}
8
9 {-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
10
11 module TcUnify (
12 -- Full-blown subsumption
13 tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
14 tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
15 tcSubTypeDS_NC_O, tcSubTypeET,
16 checkConstraints, checkTvConstraints,
17 buildImplicationFor,
18
19 -- Various unifications
20 unifyType, unifyTheta, unifyKind,
21 uType, promoteTcType,
22 swapOverTyVars, canSolveByUnification,
23
24 --------------------------------
25 -- Holes
26 tcInferInst, tcInferNoInst,
27 matchExpectedListTy,
28 matchExpectedTyConApp,
29 matchExpectedAppTy,
30 matchExpectedFunTys,
31 matchActualFunTys, matchActualFunTysPart,
32 matchExpectedFunKind,
33
34 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 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 Trac #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 = typeKind orig_ty
446 kind1 = mkFunTy 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 Trac #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 agressively 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. Trac #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 imprdicative types), but it
756 -- caused Trac #12616 because (also bizarrely) 'deriving' code had
757 -- -XImpredicativeTypes on. I deleted the entire case.
758
759 go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
760 | not (isPredTy act_arg)
761 , not (isPredTy exp_arg)
762 = -- See Note [Co/contra-variance of subsumption checking]
763 do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
764 ; arg_wrap <- tc_sub_tc_type eq_orig given_orig ctxt exp_arg act_arg
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 -----------------
814 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
815 -- expressions
816 tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
817 -> TcM (HsExpr GhcTcId)
818 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
819
820 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
821 -- convenient.
822 tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
823 -> TcM (HsExpr GhcTcId)
824 tcWrapResultO orig rn_expr expr actual_ty res_ty
825 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
826 , text "Expected:" <+> ppr res_ty ])
827 ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
828 (Just rn_expr) actual_ty res_ty
829 ; return (mkHsWrap cow expr) }
830
831
832 {- **********************************************************************
833 %* *
834 ExpType functions: tcInfer, fillInferResult
835 %* *
836 %********************************************************************* -}
837
838 -- | Infer a type using a fresh ExpType
839 -- See also Note [ExpType] in TcMType
840 -- Does not attempt to instantiate the inferred type
841 tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
842 tcInferNoInst = tcInfer False
843
844 tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
845 tcInferInst = tcInfer True
846
847 tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
848 tcInfer instantiate tc_check
849 = do { res_ty <- newInferExpType instantiate
850 ; result <- tc_check res_ty
851 ; res_ty <- readExpType res_ty
852 ; return (result, res_ty) }
853
854 fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
855 -- If wrap = fillInferResult t1 t2
856 -- => wrap :: t1 ~> t2
857 -- See Note [Deep instantiation of InferResult]
858 fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
859 | instantiate_me
860 = do { (wrap, rho) <- deeplyInstantiate orig ty
861 ; co <- fill_infer_result rho inf_res
862 ; return (mkWpCastN co <.> wrap) }
863
864 | otherwise
865 = do { co <- fill_infer_result ty inf_res
866 ; return (mkWpCastN co) }
867
868 fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
869 -- If wrap = fill_infer_result t1 t2
870 -- => wrap :: t1 ~> t2
871 fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
872 , ir_ref = ref })
873 = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
874
875 ; traceTc "Filling ExpType" $
876 ppr u <+> text ":=" <+> ppr ty_to_fill_with
877
878 ; when debugIsOn (check_hole ty_to_fill_with)
879
880 ; writeTcRef ref (Just ty_to_fill_with)
881
882 ; return ty_co }
883 where
884 check_hole ty -- Debug check only
885 = do { let ty_lvl = tcTypeLevel ty
886 ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
887 ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
888 ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty )
889 ; cts <- readTcRef ref
890 ; case cts of
891 Just already_there -> pprPanic "writeExpType"
892 (vcat [ ppr u
893 , ppr ty
894 , ppr already_there ])
895 Nothing -> return () }
896
897 {- Note [Deep instantiation of InferResult]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 In some cases we want to deeply instantiate before filling in
900 an InferResult, and in some cases not. That's why InferReult
901 has the ir_inst flag.
902
903 * ir_inst = True: deeply instantiate
904
905 Consider
906 f x = (*)
907 We want to instantiate the type of (*) before returning, else we
908 will infer the type
909 f :: forall {a}. a -> forall b. Num b => b -> b -> b
910 This is surely confusing for users.
911
912 And worse, the monomorphism restriction won't properly. The MR is
913 dealt with in simplifyInfer, and simplifyInfer has no way of
914 instantiating. This could perhaps be worked around, but it may be
915 hard to know even when instantiation should happen.
916
917 Another reason. Consider
918 f :: (?x :: Int) => a -> a
919 g y = let ?x = 3::Int in f
920 Here want to instantiate f's type so that the ?x::Int constraint
921 gets discharged by the enclosing implicit-parameter binding.
922
923 * ir_inst = False: do not instantiate
924
925 Consider this (which uses visible type application):
926
927 (let { f :: forall a. a -> a; f x = x } in f) @Int
928
929 We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
930 And we don't want to instantite the type of 'f' when we reach it,
931 else the outer visible type application won't work
932 -}
933
934 {- *********************************************************************
935 * *
936 Promoting types
937 * *
938 ********************************************************************* -}
939
940 promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
941 -- See Note [Promoting a type]
942 -- promoteTcType level ty = (co, ty')
943 -- * Returns ty' whose max level is just 'level'
944 -- and whose kind is ~# to the kind of 'ty'
945 -- and whose kind has form TYPE rr
946 -- * and co :: ty ~ ty'
947 -- * and emits constraints to justify the coercion
948 promoteTcType dest_lvl ty
949 = do { cur_lvl <- getTcLevel
950 ; if (cur_lvl `sameDepthAs` dest_lvl)
951 then dont_promote_it
952 else promote_it }
953 where
954 promote_it :: TcM (TcCoercion, TcType)
955 promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
956 -- where alpha and rr are fresh and from level dest_lvl
957 = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
958 ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
959 ; let eq_orig = TypeEqOrigin { uo_actual = ty
960 , uo_expected = prom_ty
961 , uo_thing = Nothing
962 , uo_visible = False }
963
964 ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
965 ; return (co, prom_ty) }
966
967 dont_promote_it :: TcM (TcCoercion, TcType)
968 dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
969 = do { res_kind <- newOpenTypeKind
970 ; let ty_kind = typeKind ty
971 kind_orig = TypeEqOrigin { uo_actual = ty_kind
972 , uo_expected = res_kind
973 , uo_thing = Nothing
974 , uo_visible = False }
975 ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
976 ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
977 ; return (co, ty `mkCastTy` ki_co) }
978
979 {- Note [Promoting a type]
980 ~~~~~~~~~~~~~~~~~~~~~~~~~~
981 Consider (Trac #12427)
982
983 data T where
984 MkT :: (Int -> Int) -> a -> T
985
986 h y = case y of MkT v w -> v
987
988 We'll infer the RHS type with an expected type ExpType of
989 (IR { ir_lvl = l, ir_ref = ref, ... )
990 where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
991 match will increase the level, so we'll end up in tcSubType, trying to
992 unify the type of v,
993 v :: Int -> Int
994 with the expected type. But this attempt takes place at level (l+1),
995 rightly so, since v's type could have mentioned existential variables,
996 (like w's does) and we want to catch that.
997
998 So we
999 - create a new meta-var alpha[l+1]
1000 - fill in the InferRes ref cell 'ref' with alpha
1001 - emit an equality constraint, thus
1002 [W] alpha[l+1] ~ (Int -> Int)
1003
1004 That constraint will float outwards, as it should, unless v's
1005 type mentions a skolem-captured variable.
1006
1007 This approach fails if v has a higher rank type; see
1008 Note [Promotion and higher rank types]
1009
1010
1011 Note [Promotion and higher rank types]
1012 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1013 If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
1014 then we'd emit an equality
1015 [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
1016 which will sadly fail because we can't unify a unification variable
1017 with a polytype. But there is nothing really wrong with the program
1018 here.
1019
1020 We could just about solve this by "promote the type" of v, to expose
1021 its polymorphic "shape" while still leaving constraints that will
1022 prevent existential escape. But we must be careful! Exposing
1023 the "shape" of the type is precisely what we must NOT do under
1024 a GADT pattern match! So in this case we might promote the type
1025 to
1026 (forall a. a->a) -> alpha[l+1]
1027 and emit the constraint
1028 [W] alpha[l+1] ~ Int
1029 Now the poromoted type can fill the ref cell, while the emitted
1030 equality can float or not, according to the usual rules.
1031
1032 But that's not quite right! We are exposing the arrow! We could
1033 deal with that too:
1034 (forall a. mu[l+1] a a) -> alpha[l+1]
1035 with constraints
1036 [W] alpha[l+1] ~ Int
1037 [W] mu[l+1] ~ (->)
1038 Here we abstract over the '->' inside the forall, in case that
1039 is subject to an equality constraint from a GADT match.
1040
1041 Note that we kept the outer (->) because that's part of
1042 the polymorphic "shape". And becauuse of impredicativity,
1043 GADT matches can't give equalities that affect polymorphic
1044 shape.
1045
1046 This reasoning just seems too complicated, so I decided not
1047 to do it. These higher-rank notes are just here to record
1048 the thinking.
1049 -}
1050
1051 {- *********************************************************************
1052 * *
1053 Generalisation
1054 * *
1055 ********************************************************************* -}
1056
1057 -- | Take an "expected type" and strip off quantifiers to expose the
1058 -- type underneath, binding the new skolems for the @thing_inside@.
1059 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
1060 tcSkolemise :: UserTypeCtxt -> TcSigmaType
1061 -> ([TcTyVar] -> TcType -> TcM result)
1062 -- ^ These are only ever used for scoped type variables.
1063 -> TcM (HsWrapper, result)
1064 -- ^ The expression has type: spec_ty -> expected_ty
1065
1066 tcSkolemise ctxt expected_ty thing_inside
1067 -- We expect expected_ty to be a forall-type
1068 -- If not, the call is a no-op
1069 = do { traceTc "tcSkolemise" Outputable.empty
1070 ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty
1071
1072 ; lvl <- getTcLevel
1073 ; when debugIsOn $
1074 traceTc "tcSkolemise" $ vcat [
1075 ppr lvl,
1076 text "expected_ty" <+> ppr expected_ty,
1077 text "inst tyvars" <+> ppr tv_prs,
1078 text "given" <+> ppr given,
1079 text "inst type" <+> ppr rho' ]
1080
1081 -- Generally we must check that the "forall_tvs" havn't been constrained
1082 -- The interesting bit here is that we must include the free variables
1083 -- of the expected_ty. Here's an example:
1084 -- runST (newVar True)
1085 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
1086 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
1087 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
1088 -- So now s' isn't unconstrained because it's linked to a.
1089 --
1090 -- However [Oct 10] now that the untouchables are a range of
1091 -- TcTyVars, all this is handled automatically with no need for
1092 -- extra faffing around
1093
1094 ; let tvs' = map snd tv_prs
1095 skol_info = SigSkol ctxt expected_ty tv_prs
1096
1097 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
1098 thing_inside tvs' rho'
1099
1100 ; return (wrap <.> mkWpLet ev_binds, result) }
1101 -- The ev_binds returned by checkConstraints is very
1102 -- often empty, in which case mkWpLet is a no-op
1103
1104 -- | Variant of 'tcSkolemise' that takes an ExpType
1105 tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
1106 -> (ExpRhoType -> TcM result)
1107 -> TcM (HsWrapper, result)
1108 tcSkolemiseET _ et@(Infer {}) thing_inside
1109 = (idHsWrapper, ) <$> thing_inside et
1110 tcSkolemiseET ctxt (Check ty) thing_inside
1111 = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType
1112
1113 checkConstraints :: SkolemInfo
1114 -> [TcTyVar] -- Skolems
1115 -> [EvVar] -- Given
1116 -> TcM result
1117 -> TcM (TcEvBinds, result)
1118
1119 checkConstraints skol_info skol_tvs given thing_inside
1120 = do { implication_needed <- implicationNeeded skol_tvs given
1121
1122 ; if implication_needed
1123 then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
1124 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
1125 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
1126 ; emitImplications implics
1127 ; return (ev_binds, result) }
1128
1129 else -- Fast path. We check every function argument with
1130 -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
1131 -- So this fast path is well-exercised
1132 do { res <- thing_inside
1133 ; return (emptyTcEvBinds, res) } }
1134
1135 checkTvConstraints :: SkolemInfo
1136 -> Maybe SDoc -- User-written telescope, if present
1137 -> TcM ([TcTyVar], result)
1138 -> TcM ([TcTyVar], result)
1139
1140 checkTvConstraints skol_info m_telescope thing_inside
1141 = do { (tclvl, wanted, (skol_tvs, result))
1142 <- pushLevelAndCaptureConstraints thing_inside
1143
1144 ; if isEmptyWC wanted
1145 then return ()
1146 else do { tc_lcl_env <- getLclEnv
1147 ; ev_binds <- newNoTcEvBinds
1148 ; emitImplication $
1149 newImplication { ic_tclvl = tclvl
1150 , ic_skols = skol_tvs
1151 , ic_no_eqs = True
1152 , ic_telescope = m_telescope
1153 , ic_wanted = wanted
1154 , ic_binds = ev_binds
1155 , ic_info = skol_info
1156 , ic_env = tc_lcl_env } }
1157 ; return (skol_tvs, result) }
1158
1159
1160 implicationNeeded :: [TcTyVar] -> [EvVar] -> TcM Bool
1161 -- With the solver producing unlifted equalities, we need
1162 -- to have an EvBindsVar for them when they might be deferred to
1163 -- runtime. Otherwise, they end up as top-level unlifted bindings,
1164 -- which are verboten. See also Note [Deferred errors for coercion holes]
1165 -- in TcErrors. cf Trac #14149 for an example of what goes wrong.
1166 implicationNeeded skol_tvs given
1167 | null skol_tvs
1168 , null given
1169 = -- Empty skolems and givens
1170 do { tc_lvl <- getTcLevel
1171 ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
1172 then return False -- already inside an implication
1173 else
1174 do { dflags <- getDynFlags -- If any deferral can happen,
1175 -- we must build an implication
1176 ; return (gopt Opt_DeferTypeErrors dflags ||
1177 gopt Opt_DeferTypedHoles dflags ||
1178 gopt Opt_DeferOutOfScopeVariables dflags) } }
1179
1180 | otherwise -- Non-empty skolems or givens
1181 = return True -- Definitely need an implication
1182
1183 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
1184 -> [EvVar] -> WantedConstraints
1185 -> TcM (Bag Implication, TcEvBinds)
1186 buildImplicationFor tclvl skol_info skol_tvs given wanted
1187 | isEmptyWC wanted && null given
1188 -- Optimisation : if there are no wanteds, and no givens
1189 -- don't generate an implication at all.
1190 -- Reason for the (null given): we don't want to lose
1191 -- the "inaccessible alternative" error check
1192 = return (emptyBag, emptyTcEvBinds)
1193
1194 | otherwise
1195 = ASSERT2( all (isSkolemTyVar <||> isSigTyVar) skol_tvs, ppr skol_tvs )
1196 -- Why allow SigTvs? Because implicitly declared kind variables in
1197 -- non-CUSK type declarations are SigTvs, and we need to bring them
1198 -- into scope as a skolem in an implication. This is OK, though,
1199 -- because SigTvs will always remain tyvars, even after unification.
1200 do { ev_binds_var <- newTcEvBinds
1201 ; env <- getLclEnv
1202 ; let implic = newImplication { ic_tclvl = tclvl
1203 , ic_skols = skol_tvs
1204 , ic_given = given
1205 , ic_wanted = wanted
1206 , ic_binds = ev_binds_var
1207 , ic_env = env
1208 , ic_info = skol_info }
1209
1210 ; return (unitBag implic, TcEvBinds ev_binds_var) }
1211
1212 {-
1213 ************************************************************************
1214 * *
1215 Boxy unification
1216 * *
1217 ************************************************************************
1218
1219 The exported functions are all defined as versions of some
1220 non-exported generic functions.
1221 -}
1222
1223 unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1'
1224 -> TcTauType -> TcTauType -> TcM TcCoercionN
1225 -- Actual and expected types
1226 -- Returns a coercion : ty1 ~ ty2
1227 unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
1228 uType TypeLevel origin ty1 ty2
1229 where
1230 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
1231 , uo_thing = ppr <$> thing
1232 , uo_visible = True } -- always called from a visible context
1233
1234 unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
1235 unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
1236 uType KindLevel origin ty1 ty2
1237 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
1238 , uo_thing = ppr <$> thing
1239 , uo_visible = True } -- also always from a visible context
1240
1241 ---------------
1242 unifyPred :: PredType -> PredType -> TcM TcCoercionN
1243 -- Actual and expected types
1244 unifyPred = unifyType Nothing
1245
1246 ---------------
1247 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
1248 -- Actual and expected types
1249 unifyTheta theta1 theta2
1250 = do { checkTc (equalLength theta1 theta2)
1251 (vcat [text "Contexts differ in length",
1252 nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"])
1253 ; zipWithM unifyPred theta1 theta2 }
1254
1255 {-
1256 %************************************************************************
1257 %* *
1258 uType and friends
1259 %* *
1260 %************************************************************************
1261
1262 uType is the heart of the unifier.
1263 -}
1264
1265 uType, uType_defer
1266 :: TypeOrKind
1267 -> CtOrigin
1268 -> TcType -- ty1 is the *actual* type
1269 -> TcType -- ty2 is the *expected* type
1270 -> TcM Coercion
1271
1272 --------------
1273 -- It is always safe to defer unification to the main constraint solver
1274 -- See Note [Deferred unification]
1275 uType_defer t_or_k origin ty1 ty2
1276 = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
1277
1278 -- Error trace only
1279 -- NB. do *not* call mkErrInfo unless tracing is on,
1280 -- because it is hugely expensive (#5631)
1281 ; whenDOptM Opt_D_dump_tc_trace $ do
1282 { ctxt <- getErrCtxt
1283 ; doc <- mkErrInfo emptyTidyEnv ctxt
1284 ; traceTc "utype_defer" (vcat [ debugPprType ty1
1285 , debugPprType ty2
1286 , pprCtOrigin origin
1287 , doc])
1288 ; traceTc "utype_defer2" (ppr co)
1289 }
1290 ; return co }
1291
1292 --------------
1293 uType t_or_k origin orig_ty1 orig_ty2
1294 = do { tclvl <- getTcLevel
1295 ; traceTc "u_tys" $ vcat
1296 [ text "tclvl" <+> ppr tclvl
1297 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
1298 , pprCtOrigin origin]
1299 ; co <- go orig_ty1 orig_ty2
1300 ; if isReflCo co
1301 then traceTc "u_tys yields no coercion" Outputable.empty
1302 else traceTc "u_tys yields coercion:" (ppr co)
1303 ; return co }
1304 where
1305 go :: TcType -> TcType -> TcM Coercion
1306 -- The arguments to 'go' are always semantically identical
1307 -- to orig_ty{1,2} except for looking through type synonyms
1308
1309 -- Variables; go for uVar
1310 -- Note that we pass in *original* (before synonym expansion),
1311 -- so that type variables tend to get filled in with
1312 -- the most informative version of the type
1313 go (TyVarTy tv1) ty2
1314 = do { lookup_res <- lookupTcTyVar tv1
1315 ; case lookup_res of
1316 Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
1317 ; go ty1 ty2 }
1318 Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
1319 go ty1 (TyVarTy tv2)
1320 = do { lookup_res <- lookupTcTyVar tv2
1321 ; case lookup_res of
1322 Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
1323 ; go ty1 ty2 }
1324 Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
1325
1326 -- See Note [Expanding synonyms during unification]
1327 go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
1328 | tc1 == tc2
1329 = return $ mkReflCo Nominal ty1
1330
1331 go (CastTy t1 co1) t2
1332 = do { co_tys <- go t1 t2
1333 ; return (mkCoherenceLeftCo co_tys co1) }
1334
1335 go t1 (CastTy t2 co2)
1336 = do { co_tys <- go t1 t2
1337 ; return (mkCoherenceRightCo co_tys co2) }
1338
1339 -- See Note [Expanding synonyms during unification]
1340 --
1341 -- Also NB that we recurse to 'go' so that we don't push a
1342 -- new item on the origin stack. As a result if we have
1343 -- type Foo = Int
1344 -- and we try to unify Foo ~ Bool
1345 -- we'll end up saying "can't match Foo with Bool"
1346 -- rather than "can't match "Int with Bool". See Trac #4535.
1347 go ty1 ty2
1348 | Just ty1' <- tcView ty1 = go ty1' ty2
1349 | Just ty2' <- tcView ty2 = go ty1 ty2'
1350
1351 -- Functions (or predicate functions) just check the two parts
1352 go (FunTy fun1 arg1) (FunTy fun2 arg2)
1353 = do { co_l <- uType t_or_k origin fun1 fun2
1354 ; co_r <- uType t_or_k origin arg1 arg2
1355 ; return $ mkFunCo Nominal co_l co_r }
1356
1357 -- Always defer if a type synonym family (type function)
1358 -- is involved. (Data families behave rigidly.)
1359 go ty1@(TyConApp tc1 _) ty2
1360 | isTypeFamilyTyCon tc1 = defer ty1 ty2
1361 go ty1 ty2@(TyConApp tc2 _)
1362 | isTypeFamilyTyCon tc2 = defer ty1 ty2
1363
1364 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1365 -- See Note [Mismatched type lists and application decomposition]
1366 | tc1 == tc2, equalLength tys1 tys2
1367 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
1368 do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
1369 ; return $ mkTyConAppCo Nominal tc1 cos }
1370 where
1371 origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
1372 (tcTyConVisibilities tc1)
1373
1374 go (LitTy m) ty@(LitTy n)
1375 | m == n
1376 = return $ mkNomReflCo ty
1377
1378 -- See Note [Care with type applications]
1379 -- Do not decompose FunTy against App;
1380 -- it's often a type error, so leave it for the constraint solver
1381 go (AppTy s1 t1) (AppTy s2 t2)
1382 = go_app (isNextArgVisible s1) s1 t1 s2 t2
1383
1384 go (AppTy s1 t1) (TyConApp tc2 ts2)
1385 | Just (ts2', t2') <- snocView ts2
1386 = ASSERT( mightBeUnsaturatedTyCon tc2 )
1387 go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
1388
1389 go (TyConApp tc1 ts1) (AppTy s2 t2)
1390 | Just (ts1', t1') <- snocView ts1
1391 = ASSERT( mightBeUnsaturatedTyCon tc1 )
1392 go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
1393
1394 go (CoercionTy co1) (CoercionTy co2)
1395 = do { let ty1 = coercionType co1
1396 ty2 = coercionType co2
1397 ; kco <- uType KindLevel
1398 (KindEqOrigin orig_ty1 (Just orig_ty2) origin
1399 (Just t_or_k))
1400 ty1 ty2
1401 ; return $ mkProofIrrelCo Nominal kco co1 co2 }
1402
1403 -- Anything else fails
1404 -- E.g. unifying for-all types, which is relative unusual
1405 go ty1 ty2 = defer ty1 ty2
1406
1407 ------------------
1408 defer ty1 ty2 -- See Note [Check for equality before deferring]
1409 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
1410 | otherwise = uType_defer t_or_k origin ty1 ty2
1411
1412 ------------------
1413 go_app vis s1 t1 s2 t2
1414 = do { co_s <- uType t_or_k origin s1 s2
1415 ; let arg_origin
1416 | vis = origin
1417 | otherwise = toInvisibleOrigin origin
1418 ; co_t <- uType t_or_k arg_origin t1 t2
1419 ; return $ mkAppCo co_s co_t }
1420
1421 {- Note [Check for equality before deferring]
1422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1423 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
1424 If ty involves a type function we may defer, which isn't very sensible.
1425 An egregious example of this was in test T9872a, which has a type signature
1426 Proxy :: Proxy (Solutions Cubes)
1427 Doing the ambiguity check on this signature generates the equality
1428 Solutions Cubes ~ Solutions Cubes
1429 and currently the constraint solver normalises both sides at vast cost.
1430 This little short-cut in 'defer' helps quite a bit.
1431
1432 Note [Care with type applications]
1433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1434 Note: type applications need a bit of care!
1435 They can match FunTy and TyConApp, so use splitAppTy_maybe
1436 NB: we've already dealt with type variables and Notes,
1437 so if one type is an App the other one jolly well better be too
1438
1439 Note [Mismatched type lists and application decomposition]
1440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1441 When we find two TyConApps, you might think that the argument lists
1442 are guaranteed equal length. But they aren't. Consider matching
1443 w (T x) ~ Foo (T x y)
1444 We do match (w ~ Foo) first, but in some circumstances we simply create
1445 a deferred constraint; and then go ahead and match (T x ~ T x y).
1446 This came up in Trac #3950.
1447
1448 So either
1449 (a) either we must check for identical argument kinds
1450 when decomposing applications,
1451
1452 (b) or we must be prepared for ill-kinded unification sub-problems
1453
1454 Currently we adopt (b) since it seems more robust -- no need to maintain
1455 a global invariant.
1456
1457 Note [Expanding synonyms during unification]
1458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1459 We expand synonyms during unification, but:
1460 * We expand *after* the variable case so that we tend to unify
1461 variables with un-expanded type synonym. This just makes it
1462 more likely that the inferred types will mention type synonyms
1463 understandable to the user
1464
1465 * Similarly, we expand *after* the CastTy case, just in case the
1466 CastTy wraps a variable.
1467
1468 * We expand *before* the TyConApp case. For example, if we have
1469 type Phantom a = Int
1470 and are unifying
1471 Phantom Int ~ Phantom Char
1472 it is *wrong* to unify Int and Char.
1473
1474 * The problem case immediately above can happen only with arguments
1475 to the tycon. So we check for nullary tycons *before* expanding.
1476 This is particularly helpful when checking (* ~ *), because * is
1477 now a type synonym.
1478
1479 Note [Deferred Unification]
1480 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1481 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
1482 and yet its consistency is undetermined. Previously, there was no way to still
1483 make it consistent. So a mismatch error was issued.
1484
1485 Now these unifications are deferred until constraint simplification, where type
1486 family instances and given equations may (or may not) establish the consistency.
1487 Deferred unifications are of the form
1488 F ... ~ ...
1489 or x ~ ...
1490 where F is a type function and x is a type variable.
1491 E.g.
1492 id :: x ~ y => x -> y
1493 id e = e
1494
1495 involves the unification x = y. It is deferred until we bring into account the
1496 context x ~ y to establish that it holds.
1497
1498 If available, we defer original types (rather than those where closed type
1499 synonyms have already been expanded via tcCoreView). This is, as usual, to
1500 improve error messages.
1501
1502
1503 ************************************************************************
1504 * *
1505 uVar and friends
1506 * *
1507 ************************************************************************
1508
1509 @uVar@ is called when at least one of the types being unified is a
1510 variable. It does {\em not} assume that the variable is a fixed point
1511 of the substitution; rather, notice that @uVar@ (defined below) nips
1512 back into @uTys@ if it turns out that the variable is already bound.
1513 -}
1514
1515 ----------
1516 uUnfilledVar :: CtOrigin
1517 -> TypeOrKind
1518 -> SwapFlag
1519 -> TcTyVar -- Tyvar 1
1520 -> TcTauType -- Type 2
1521 -> TcM Coercion
1522 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
1523 -- It might be a skolem, or untouchable, or meta
1524
1525 uUnfilledVar origin t_or_k swapped tv1 ty2
1526 = do { ty2 <- zonkTcType ty2
1527 -- Zonk to expose things to the
1528 -- occurs check, and so that if ty2
1529 -- looks like a type variable then it
1530 -- /is/ a type variable
1531 ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
1532
1533 ----------
1534 uUnfilledVar1 :: CtOrigin
1535 -> TypeOrKind
1536 -> SwapFlag
1537 -> TcTyVar -- Tyvar 1
1538 -> TcTauType -- Type 2, zonked
1539 -> TcM Coercion
1540 uUnfilledVar1 origin t_or_k swapped tv1 ty2
1541 | Just tv2 <- tcGetTyVar_maybe ty2
1542 = go tv2
1543
1544 | otherwise
1545 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1546
1547 where
1548 -- 'go' handles the case where both are
1549 -- tyvars so we might want to swap
1550 go tv2 | tv1 == tv2 -- Same type variable => no-op
1551 = return (mkNomReflCo (mkTyVarTy tv1))
1552
1553 | swapOverTyVars tv1 tv2 -- Distinct type variables
1554 = uUnfilledVar2 origin t_or_k (flipSwap swapped)
1555 tv2 (mkTyVarTy tv1)
1556
1557 | otherwise
1558 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1559
1560 ----------
1561 uUnfilledVar2 :: CtOrigin
1562 -> TypeOrKind
1563 -> SwapFlag
1564 -> TcTyVar -- Tyvar 1
1565 -> TcTauType -- Type 2, zonked
1566 -> TcM Coercion
1567 uUnfilledVar2 origin t_or_k swapped tv1 ty2
1568 = do { dflags <- getDynFlags
1569 ; cur_lvl <- getTcLevel
1570 ; go dflags cur_lvl }
1571 where
1572 go dflags cur_lvl
1573 | canSolveByUnification cur_lvl tv1 ty2
1574 , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
1575 = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
1576 ; if isTcReflCo co_k -- only proceed if the kinds matched.
1577
1578 then do { writeMetaTyVar tv1 ty2'
1579 ; return (mkTcNomReflCo ty2') }
1580 else defer } -- this cannot be solved now.
1581 -- See Note [Equalities with incompatible kinds]
1582 -- in TcCanonical
1583
1584 | otherwise
1585 = defer
1586 -- Occurs check or an untouchable: just defer
1587 -- NB: occurs check isn't necessarily fatal:
1588 -- eg tv1 occured in type family parameter
1589
1590 ty1 = mkTyVarTy tv1
1591 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
1592
1593 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
1594
1595 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
1596 swapOverTyVars tv1 tv2
1597 -- Level comparison: see Note [TyVar/TyVar orientation]
1598 | lvl1 `strictlyDeeperThan` lvl2 = False
1599 | lvl2 `strictlyDeeperThan` lvl1 = True
1600
1601 -- Priority: see Note [TyVar/TyVar orientation]
1602 | pri1 > pri2 = False
1603 | pri2 > pri1 = True
1604
1605 -- Names: see Note [TyVar/TyVar orientation]
1606 | isSystemName tv2_name, not (isSystemName tv1_name) = True
1607
1608 | otherwise = False
1609
1610 where
1611 lvl1 = tcTyVarLevel tv1
1612 lvl2 = tcTyVarLevel tv2
1613 pri1 = lhsPriority tv1
1614 pri2 = lhsPriority tv2
1615 tv1_name = Var.varName tv1
1616 tv2_name = Var.varName tv2
1617
1618
1619 lhsPriority :: TcTyVar -> Int
1620 -- Higher => more important to be on the LHS
1621 -- See Note [TyVar/TyVar orientation]
1622 lhsPriority tv
1623 = ASSERT2( isTyVar tv, ppr tv)
1624 case tcTyVarDetails tv of
1625 RuntimeUnk -> 0
1626 SkolemTv {} -> 0
1627 MetaTv { mtv_info = info } -> case info of
1628 FlatSkolTv -> 1
1629 SigTv -> 2
1630 TauTv -> 3
1631 FlatMetaTv -> 4
1632 {- Note [TyVar/TyVar orientation]
1633 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1634 Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
1635 This is a surprisingly tricky question!
1636
1637 First note: only swap if you have to!
1638 See Note [Avoid unnecessary swaps]
1639
1640 So we look for a positive reason to swap, using a three-step test:
1641
1642 * Level comparison. If 'a' has deeper level than 'b',
1643 put 'a' on the left. See Note [Deeper level on the left]
1644
1645 * Priority. If the levels are the same, look at what kind of
1646 type variable it is, using 'lhsPriority'
1647
1648 - FlatMetaTv: Always put on the left.
1649 See Note [Fmv Orientation Invariant]
1650 NB: FlatMetaTvs always have the current level, never an
1651 outer one. So nothing can be deeper than a FlatMetaTv
1652
1653
1654 - SigTv/TauTv: if we have sig_tv ~ tau_tv, put tau_tv
1655 on the left because there are fewer
1656 restrictions on updating TauTvs
1657
1658 - SigTv/TauTv: put on the left eitehr
1659 a) Because it's touchable and can be unified, or
1660 b) Even if it's not touchable, TcSimplify.floatEqualities
1661 looks for meta tyvars on the left
1662
1663 - FlatSkolTv: Put on the left in preference to a SkolemTv
1664 See Note [Eliminate flat-skols]
1665
1666 * Names. If the level and priority comparisons are all
1667 equal, try to eliminate a TyVars with a System Name in
1668 favour of ones with a Name derived from a user type signature
1669
1670 * Age. At one point in the past we tried to break any remaining
1671 ties by eliminating the younger type variable, based on their
1672 Uniques. See Note [Eliminate younger unification variables]
1673 (which also explains why we don't do this any more)
1674
1675 Note [Deeper level on the left]
1676 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1677 The most important thing is that we want to put tyvars with
1678 the deepest level on the left. The reason to do so differs for
1679 Wanteds and Givens, but either way, deepest wins! Simple.
1680
1681 * Wanteds. Putting the deepest variable on the left maximise the
1682 chances that it's a touchable meta-tyvar which can be solved.
1683
1684 * Givens. Suppose we have something like
1685 forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
1686
1687 If we orient the Given a[2] on the left, we'll rewrite the Wanted to
1688 (beta[1] ~ b[1]), and that can float out of the implication.
1689 Otherwise it can't. By putting the deepest variable on the left
1690 we maximise our changes of elminating skolem capture.
1691
1692 See also TcSMonad Note [Let-bound skolems] for another reason
1693 to orient with the deepest skolem on the left.
1694
1695 IMPORTANT NOTE: this test does a level-number comparison on
1696 skolems, so it's important that skolems have (accurate) level
1697 numbers.
1698
1699 See Trac #15009 for an further analysis of why "deepest on the left"
1700 is a good plan.
1701
1702 Note [Fmv Orientation Invariant]
1703 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1704 * We always orient a constraint
1705 fmv ~ alpha
1706 with fmv on the left, even if alpha is
1707 a touchable unification variable
1708
1709 Reason: doing it the other way round would unify alpha:=fmv, but that
1710 really doesn't add any info to alpha. But a later constraint alpha ~
1711 Int might unlock everything. Comment:9 of #12526 gives a detailed
1712 example.
1713
1714 WARNING: I've gone to and fro on this one several times.
1715 I'm now pretty sure that unifying alpha:=fmv is a bad idea!
1716 So orienting with fmvs on the left is a good thing.
1717
1718 This example comes from IndTypesPerfMerge. (Others include
1719 T10226, T10009.)
1720 From the ambiguity check for
1721 f :: (F a ~ a) => a
1722 we get:
1723 [G] F a ~ a
1724 [WD] F alpha ~ alpha, alpha ~ a
1725
1726 From Givens we get
1727 [G] F a ~ fsk, fsk ~ a
1728
1729 Now if we flatten we get
1730 [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
1731
1732 Now, if we unified alpha := fmv, we'd get
1733 [WD] F fmv ~ fmv, [WD] fmv ~ a
1734 And now we are stuck.
1735
1736 So instead the Fmv Orientation Invariant puts the fmv on the
1737 left, giving
1738 [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
1739
1740 Now we get alpha:=a, and everything works out
1741
1742 Note [Eliminate flat-skols]
1743 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1744 Suppose we have [G] Num (F [a])
1745 then we flatten to
1746 [G] Num fsk
1747 [G] F [a] ~ fsk
1748 where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
1749 type instance F [a] = a
1750 then we'll reduce the second constraint to
1751 [G] a ~ fsk
1752 and then replace all uses of 'a' with fsk. That's bad because
1753 in error messages intead of saying 'a' we'll say (F [a]). In all
1754 places, including those where the programmer wrote 'a' in the first
1755 place. Very confusing! See Trac #7862.
1756
1757 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1758 the fsk.
1759
1760 Note [Avoid unnecessary swaps]
1761 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1762 If we swap without actually improving matters, we can get an infinite loop.
1763 Consider
1764 work item: a ~ b
1765 inert item: b ~ c
1766 We canonicalise the work-item to (a ~ c). If we then swap it before
1767 adding to the inert set, we'll add (c ~ a), and therefore kick out the
1768 inert guy, so we get
1769 new work item: b ~ c
1770 inert item: c ~ a
1771 And now the cycle just repeats
1772
1773 Note [Eliminate younger unification variables]
1774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1775 Given a choice of unifying
1776 alpha := beta or beta := alpha
1777 we try, if possible, to elimiate the "younger" one, as determined
1778 by `ltUnique`. Reason: the younger one is less likely to appear free in
1779 an existing inert constraint, and hence we are less likely to be forced
1780 into kicking out and rewriting inert constraints.
1781
1782 This is a performance optimisation only. It turns out to fix
1783 Trac #14723 all by itself, but clearly not reliably so!
1784
1785 It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars).
1786 But, to my surprise, it didn't seem to make any significant difference
1787 to the compiler's performance, so I didn't take it any further. Still
1788 it seemed to too nice to discard altogether, so I'm leaving these
1789 notes. SLPJ Jan 18.
1790 -}
1791
1792 -- @trySpontaneousSolve wi@ solves equalities where one side is a
1793 -- touchable unification variable.
1794 -- Returns True <=> spontaneous solve happened
1795 canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
1796 canSolveByUnification tclvl tv xi
1797 | isTouchableMetaTyVar tclvl tv
1798 = case metaTyVarInfo tv of
1799 SigTv -> is_tyvar xi
1800 _ -> True
1801
1802 | otherwise -- Untouchable
1803 = False
1804 where
1805 is_tyvar xi
1806 = case tcGetTyVar_maybe xi of
1807 Nothing -> False
1808 Just tv -> case tcTyVarDetails tv of
1809 MetaTv { mtv_info = info }
1810 -> case info of
1811 SigTv -> True
1812 _ -> False
1813 SkolemTv {} -> True
1814 RuntimeUnk -> True
1815
1816 {- Note [Prevent unification with type families]
1817 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1818 We prevent unification with type families because of an uneasy compromise.
1819 It's perfectly sound to unify with type families, and it even improves the
1820 error messages in the testsuite. It also modestly improves performance, at
1821 least in some cases. But it's disastrous for test case perf/compiler/T3064.
1822 Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
1823 What do we do? Do we reduce F? Or do we use the given? Hard to know what's
1824 best. GHC reduces. This is a disaster for T3064, where the type's size
1825 spirals out of control during reduction. (We're not helped by the fact that
1826 the flattener re-flattens all the arguments every time around.) If we prevent
1827 unification with type families, then the solver happens to use the equality
1828 before expanding the type family.
1829
1830 It would be lovely in the future to revisit this problem and remove this
1831 extra, unnecessary check. But we retain it for now as it seems to work
1832 better in practice.
1833
1834 Note [Refactoring hazard: checkTauTvUpdate]
1835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1836 I (Richard E.) have a sad story about refactoring this code, retained here
1837 to prevent others (or a future me!) from falling into the same traps.
1838
1839 It all started with #11407, which was caused by the fact that the TyVarTy
1840 case of defer_me didn't look in the kind. But it seemed reasonable to
1841 simply remove the defer_me check instead.
1842
1843 It referred to two Notes (since removed) that were out of date, and the
1844 fast_check code in occurCheckExpand seemed to do just about the same thing as
1845 defer_me. The one piece that defer_me did that wasn't repeated by
1846 occurCheckExpand was the type-family check. (See Note [Prevent unification
1847 with type families].) So I checked the result of occurCheckExpand for any
1848 type family occurrences and deferred if there were any. This was done
1849 in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
1850
1851 This approach turned out not to be performant, because the expanded
1852 type was bigger than the original type, and tyConsOfType (needed to
1853 see if there are any type family occurrences) looks through type
1854 synonyms. So it then struck me that we could dispense with the
1855 defer_me check entirely. This simplified the code nicely, and it cut
1856 the allocations in T5030 by half. But, as documented in Note [Prevent
1857 unification with type families], this destroyed performance in
1858 T3064. Regardless, I missed this regression and the change was
1859 committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
1860
1861 Bottom lines:
1862 * defer_me is back, but now fixed w.r.t. #11407.
1863 * Tread carefully before you start to refactor here. There can be
1864 lots of hard-to-predict consequences.
1865
1866 Note [Type synonyms and the occur check]
1867 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1868 Generally speaking we try to update a variable with type synonyms not
1869 expanded, which improves later error messages, unless looking
1870 inside a type synonym may help resolve a spurious occurs check
1871 error. Consider:
1872 type A a = ()
1873
1874 f :: (A a -> a -> ()) -> ()
1875 f = \ _ -> ()
1876
1877 x :: ()
1878 x = f (\ x p -> p x)
1879
1880 We will eventually get a constraint of the form t ~ A t. The ok function above will
1881 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1882 unified with the original type A t, we would lead the type checker into an infinite loop.
1883
1884 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1885 the ok function expands the synonym to detect opportunities for occurs check success using
1886 the underlying definition of the type synonym.
1887
1888 The same applies later on in the constraint interaction code; see TcInteract,
1889 function @occ_check_ok@.
1890
1891 Note [Non-TcTyVars in TcUnify]
1892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1893 Because the same code is now shared between unifying types and unifying
1894 kinds, we sometimes will see proper TyVars floating around the unifier.
1895 Example (from test case polykinds/PolyKinds12):
1896
1897 type family Apply (f :: k1 -> k2) (x :: k1) :: k2
1898 type instance Apply g y = g y
1899
1900 When checking the instance declaration, we first *kind-check* the LHS
1901 and RHS, discovering that the instance really should be
1902
1903 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
1904
1905 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
1906 as a second pass, we desugar the RHS (which is done in functions prefixed
1907 with "tc" in TcTyClsDecls"). By this time, all the kind-vars are proper
1908 TyVars, not TcTyVars, get some kind unification must happen.
1909
1910 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
1911 meta-tyvar.
1912
1913 This used to not be necessary for type-checking (that is, before * :: *)
1914 because expressions get desugared via an algorithm separate from
1915 type-checking (with wrappers, etc.). Types get desugared very differently,
1916 causing this wibble in behavior seen here.
1917 -}
1918
1919 data LookupTyVarResult -- The result of a lookupTcTyVar call
1920 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1921 | Filled TcType
1922
1923 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1924 lookupTcTyVar tyvar
1925 | MetaTv { mtv_ref = ref } <- details
1926 = do { meta_details <- readMutVar ref
1927 ; case meta_details of
1928 Indirect ty -> return (Filled ty)
1929 Flexi -> do { is_touchable <- isTouchableTcM tyvar
1930 -- Note [Unifying untouchables]
1931 ; if is_touchable then
1932 return (Unfilled details)
1933 else
1934 return (Unfilled vanillaSkolemTv) } }
1935 | otherwise
1936 = return (Unfilled details)
1937 where
1938 details = tcTyVarDetails tyvar
1939
1940 {-
1941 Note [Unifying untouchables]
1942 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1943 We treat an untouchable type variable as if it was a skolem. That
1944 ensures it won't unify with anything. It's a slight hack, because
1945 we return a made-up TcTyVarDetails, but I think it works smoothly.
1946 -}
1947
1948 -- | Breaks apart a function kind into its pieces.
1949 matchExpectedFunKind :: Outputable fun
1950 => fun -- ^ type, only for errors
1951 -> TcKind -- ^ function kind
1952 -> TcM (Coercion, TcKind, TcKind)
1953 -- ^ co :: old_kind ~ arg -> res
1954 matchExpectedFunKind hs_ty = go
1955 where
1956 go k | Just k' <- tcView k = go k'
1957
1958 go k@(TyVarTy kvar)
1959 | isMetaTyVar kvar
1960 = do { maybe_kind <- readMetaTyVar kvar
1961 ; case maybe_kind of
1962 Indirect fun_kind -> go fun_kind
1963 Flexi -> defer k }
1964
1965 go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
1966 go other = defer other
1967
1968 defer k
1969 = do { arg_kind <- newMetaKindVar
1970 ; res_kind <- newMetaKindVar
1971 ; let new_fun = mkFunTy arg_kind res_kind
1972 origin = TypeEqOrigin { uo_actual = k
1973 , uo_expected = new_fun
1974 , uo_thing = Just (ppr hs_ty)
1975 , uo_visible = True
1976 }
1977 ; co <- uType KindLevel origin k new_fun
1978 ; return (co, arg_kind, res_kind) }
1979
1980
1981 {- *********************************************************************
1982 * *
1983 Occurrence checking
1984 * *
1985 ********************************************************************* -}
1986
1987
1988 {- Note [Occurs check expansion]
1989 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1990 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1991 of occurrences of tv outside type function arguments, if that is
1992 possible; otherwise, it returns Nothing.
1993
1994 For example, suppose we have
1995 type F a b = [a]
1996 Then
1997 occCheckExpand b (F Int b) = Just [Int]
1998 but
1999 occCheckExpand a (F a Int) = Nothing
2000
2001 We don't promise to do the absolute minimum amount of expanding
2002 necessary, but we try not to do expansions we don't need to. We
2003 prefer doing inner expansions first. For example,
2004 type F a b = (a, Int, a, [a])
2005 type G b = Char
2006 We have
2007 occCheckExpand b (F (G b)) = Just (F Char)
2008 even though we could also expand F to get rid of b.
2009
2010 The two variants of the function are to support TcUnify.checkTauTvUpdate,
2011 which wants to prevent unification with type families. For more on this
2012 point, see Note [Prevent unification with type families] in TcUnify.
2013
2014 Note [Occurrence checking: look inside kinds]
2015 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2016 Suppose we are considering unifying
2017 (alpha :: *) ~ Int -> (beta :: alpha -> alpha)
2018 This may be an error (what is that alpha doing inside beta's kind?),
2019 but we must not make the mistake of actuallyy unifying or we'll
2020 build an infinite data structure. So when looking for occurrences
2021 of alpha in the rhs, we must look in the kinds of type variables
2022 that occur there.
2023
2024 NB: we may be able to remove the problem via expansion; see
2025 Note [Occurs check expansion]. So we have to try that.
2026
2027 Note [Checking for foralls]
2028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2029 Unless we have -XImpredicativeTypes (which is a totally unsupported
2030 feature), we do not want to unify
2031 alpha ~ (forall a. a->a) -> Int
2032 So we look for foralls hidden inside the type, and it's convenient
2033 to do that at the same time as the occurs check (which looks for
2034 occurrences of alpha).
2035
2036 However, it's not just a question of looking for foralls /anywhere/!
2037 Consider
2038 (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
2039 This is legal; e.g. dependent/should_compile/T11635.
2040
2041 We don't want to reject it because of the forall in beta's kind,
2042 but (see Note [Occurrence checking: look inside kinds]) we do
2043 need to look in beta's kind. So we carry a flag saying if a 'forall'
2044 is OK, and sitch the flag on when stepping inside a kind.
2045
2046 Why is it OK? Why does it not count as impredicative polymorphism?
2047 The reason foralls are bad is because we reply on "seeing" foralls
2048 when doing implicit instantiation. But the forall inside the kind is
2049 fine. We'll generate a kind equality constraint
2050 (forall k. k->*) ~ (forall k. k->*)
2051 to check that the kinds of lhs and rhs are compatible. If alpha's
2052 kind had instead been
2053 (alpha :: kappa)
2054 then this kind equality would rightly complain about unifying kappa
2055 with (forall k. k->*)
2056
2057 -}
2058
2059 data OccCheckResult a
2060 = OC_OK a
2061 | OC_Bad -- Forall or type family
2062 | OC_Occurs
2063
2064 instance Functor OccCheckResult where
2065 fmap = liftM
2066
2067 instance Applicative OccCheckResult where
2068 pure = OC_OK
2069 (<*>) = ap
2070
2071 instance Monad OccCheckResult where
2072 OC_OK x >>= k = k x
2073 OC_Bad >>= _ = OC_Bad
2074 OC_Occurs >>= _ = OC_Occurs
2075
2076 occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
2077 -- Just for error-message generation; so we return OccCheckResult
2078 -- so the caller can report the right kind of error
2079 -- Check whether
2080 -- a) the given variable occurs in the given type.
2081 -- b) there is a forall in the type (unless we have -XImpredicativeTypes)
2082 occCheckForErrors dflags tv ty
2083 = case preCheck dflags True tv ty of
2084 OC_OK _ -> OC_OK ()
2085 OC_Bad -> OC_Bad
2086 OC_Occurs -> case occCheckExpand tv ty of
2087 Nothing -> OC_Occurs
2088 Just _ -> OC_OK ()
2089
2090 ----------------
2091 metaTyVarUpdateOK :: DynFlags
2092 -> TcTyVar -- tv :: k1
2093 -> TcType -- ty :: k2
2094 -> Maybe TcType -- possibly-expanded ty
2095 -- (metaTyFVarUpdateOK tv ty)
2096 -- We are about to update the meta-tyvar tv with ty
2097 -- Check (a) that tv doesn't occur in ty (occurs check)
2098 -- (b) that ty does not have any foralls
2099 -- (in the impredicative case), or type functions
2100 --
2101 -- We have two possible outcomes:
2102 -- (1) Return the type to update the type variable with,
2103 -- [we know the update is ok]
2104 -- (2) Return Nothing,
2105 -- [the update might be dodgy]
2106 --
2107 -- Note that "Nothing" does not mean "definite error". For example
2108 -- type family F a
2109 -- type instance F Int = Int
2110 -- consider
2111 -- a ~ F a
2112 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
2113 -- we return Nothing, leaving it to the later constraint simplifier to
2114 -- sort matters out.
2115 --
2116 -- See Note [Refactoring hazard: checkTauTvUpdate]
2117
2118 metaTyVarUpdateOK dflags tv ty
2119 = case preCheck dflags False tv ty of
2120 -- False <=> type families not ok
2121 -- See Note [Prevent unification with type families]
2122 OC_OK _ -> Just ty
2123 OC_Bad -> Nothing -- forall or type function
2124 OC_Occurs -> occCheckExpand tv ty
2125
2126 preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
2127 -- A quick check for
2128 -- (a) a forall type (unless -XImpredivativeTypes)
2129 -- (b) a type family
2130 -- (c) an occurrence of the type variable (occurs check)
2131 --
2132 -- For (a) and (b) we check only the top level of the type, NOT
2133 -- inside the kinds of variables it mentions. But for (c) we do
2134 -- look in the kinds of course.
2135
2136 preCheck dflags ty_fam_ok tv ty
2137 = fast_check ty
2138 where
2139 details = tcTyVarDetails tv
2140 impredicative_ok = canUnifyWithPolyType dflags details
2141
2142 ok :: OccCheckResult ()
2143 ok = OC_OK ()
2144
2145 fast_check :: TcType -> OccCheckResult ()
2146 fast_check (TyVarTy tv')
2147 | tv == tv' = OC_Occurs
2148 | otherwise = fast_check_occ (tyVarKind tv')
2149 -- See Note [Occurrence checking: look inside kinds]
2150
2151 fast_check (TyConApp tc tys)
2152 | bad_tc tc = OC_Bad
2153 | otherwise = mapM fast_check tys >> ok
2154 fast_check (LitTy {}) = ok
2155 fast_check (FunTy a r) = fast_check a >> fast_check r
2156 fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
2157 fast_check (CastTy ty co) = fast_check ty >> fast_check_co co
2158 fast_check (CoercionTy co) = fast_check_co co
2159 fast_check (ForAllTy (TvBndr tv' _) ty)
2160 | not impredicative_ok = OC_Bad
2161 | tv == tv' = ok
2162 | otherwise = do { fast_check_occ (tyVarKind tv')
2163 ; fast_check_occ ty }
2164 -- Under a forall we look only for occurrences of
2165 -- the type variable
2166
2167 -- For kinds, we only do an occurs check; we do not worry
2168 -- about type families or foralls
2169 -- See Note [Checking for foralls]
2170 fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
2171 | otherwise = ok
2172
2173 -- For coercions, we are only doing an occurs check here;
2174 -- no bother about impredicativity in coercions, as they're
2175 -- inferred
2176 fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
2177 | otherwise = ok
2178
2179 bad_tc :: TyCon -> Bool
2180 bad_tc tc
2181 | not (impredicative_ok || isTauTyCon tc) = True
2182 | not (ty_fam_ok || isFamFreeTyCon tc) = True
2183 | otherwise = False
2184
2185 occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
2186 -- See Note [Occurs check expansion]
2187 -- We may have needed to do some type synonym unfolding in order to
2188 -- get rid of the variable (or forall), so we also return the unfolded
2189 -- version of the type, which is guaranteed to be syntactically free
2190 -- of the given type variable. If the type is already syntactically
2191 -- free of the variable, then the same type is returned.
2192 occCheckExpand tv ty
2193 = go emptyVarEnv ty
2194 where
2195 go :: VarEnv TyVar -> Type -> Maybe Type
2196 -- The VarEnv carries mappings necessary
2197 -- because of kind expansion
2198 go env (TyVarTy tv')
2199 | tv == tv' = Nothing
2200 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2201 | otherwise = do { tv'' <- go_var env tv'
2202 ; return (mkTyVarTy tv'') }
2203
2204 go _ ty@(LitTy {}) = return ty
2205 go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
2206 ; ty2' <- go env ty2
2207 ; return (mkAppTy ty1' ty2') }
2208 go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
2209 ; ty2' <- go env ty2
2210 ; return (mkFunTy ty1' ty2') }
2211 go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
2212 | tv == tv' = return ty
2213 | otherwise = do { ki' <- go env (tyVarKind tv')
2214 ; let tv'' = setTyVarKind tv' ki'
2215 env' = extendVarEnv env tv' tv''
2216 ; body' <- go env' body_ty
2217 ; return (ForAllTy (TvBndr tv'' vis) body') }
2218
2219 -- For a type constructor application, first try expanding away the
2220 -- offending variable from the arguments. If that doesn't work, next
2221 -- see if the type constructor is a type synonym, and if so, expand
2222 -- it and try again.
2223 go env ty@(TyConApp tc tys)
2224 = case mapM (go env) tys of
2225 Just tys' -> return (mkTyConApp tc tys')
2226 Nothing | Just ty' <- tcView ty -> go env ty'
2227 | otherwise -> Nothing
2228 -- Failing that, try to expand a synonym
2229
2230 go env (CastTy ty co) = do { ty' <- go env ty
2231 ; co' <- go_co env co
2232 ; return (mkCastTy ty' co') }
2233 go env (CoercionTy co) = do { co' <- go_co env co
2234 ; return (mkCoercionTy co') }
2235
2236 ------------------
2237 go_var env v = do { k' <- go env (varType v)
2238 ; return (setVarType v k') }
2239 -- Works for TyVar and CoVar
2240 -- See Note [Occurrence checking: look inside kinds]
2241
2242 ------------------
2243 go_co env (Refl r ty) = do { ty' <- go env ty
2244 ; return (mkReflCo r ty') }
2245 -- Note: Coercions do not contain type synonyms
2246 go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args
2247 ; return (mkTyConAppCo r tc args') }
2248 go_co env (AppCo co arg) = do { co' <- go_co env co
2249 ; arg' <- go_co env arg
2250 ; return (mkAppCo co' arg') }
2251 go_co env co@(ForAllCo tv' kind_co body_co)
2252 | tv == tv' = return co
2253 | otherwise = do { kind_co' <- go_co env kind_co
2254 ; let tv'' = setTyVarKind tv' $
2255 pFst (coercionKind kind_co')
2256 env' = extendVarEnv env tv' tv''
2257 ; body' <- go_co env' body_co
2258 ; return (ForAllCo tv'' kind_co' body') }
2259 go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1
2260 ; co2' <- go_co env co2
2261 ; return (mkFunCo r co1' co2') }
2262 go_co env (CoVarCo c) = do { c' <- go_var env c
2263 ; return (mkCoVarCo c') }
2264 go_co env (HoleCo h) = do { c' <- go_var env (ch_co_var h)
2265 ; return (HoleCo (h { ch_co_var = c' })) }
2266 go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
2267 ; return (mkAxiomInstCo ax ind args') }
2268 go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p
2269 ; ty1' <- go env ty1
2270 ; ty2' <- go env ty2
2271 ; return (mkUnivCo p' r ty1' ty2') }
2272 go_co env (SymCo co) = do { co' <- go_co env co
2273 ; return (mkSymCo co') }
2274 go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
2275 ; co2' <- go_co env co2
2276 ; return (mkTransCo co1' co2') }
2277 go_co env (NthCo r n co) = do { co' <- go_co env co
2278 ; return (mkNthCo r n co') }
2279 go_co env (LRCo lr co) = do { co' <- go_co env co
2280 ; return (mkLRCo lr co') }
2281 go_co env (InstCo co arg) = do { co' <- go_co env co
2282 ; arg' <- go_co env arg
2283 ; return (mkInstCo co' arg') }
2284 go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1
2285 ; co2' <- go_co env co2
2286 ; return (mkCoherenceCo co1' co2') }
2287 go_co env (KindCo co) = do { co' <- go_co env co
2288 ; return (mkKindCo co') }
2289 go_co env (SubCo co) = do { co' <- go_co env co
2290 ; return (mkSubCo co') }
2291 go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs
2292 ; return (mkAxiomRuleCo ax cs') }
2293
2294 ------------------
2295 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2296 go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
2297 go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
2298 go_prov _ p@(PluginProv _) = return p
2299
2300 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
2301 canUnifyWithPolyType dflags details
2302 = case details of
2303 MetaTv { mtv_info = SigTv } -> False
2304 MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags
2305 _other -> True
2306 -- We can have non-meta tyvars in given constraints