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