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