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