never executed always true always false
1 {-# LANGUAGE ScopedTypeVariables #-}
2 {-# LANGUAGE TupleSections #-}
3
4 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
6
7 {-
8 (c) The University of Glasgow 2006
9 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
10 -}
11
12 -- | Type subsumption and unification
13 module GHC.Tc.Utils.Unify (
14 -- Full-blown subsumption
15 tcWrapResult, tcWrapResultO, tcWrapResultMono,
16 tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
17 tcSubType, tcSubTypeSigma, tcSubTypePat,
18 tcSubMult,
19 checkConstraints, checkTvConstraints,
20 buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
21
22 -- Various unifications
23 unifyType, unifyKind, unifyExpectedType,
24 uType, promoteTcType,
25 swapOverTyVars, canSolveByUnification,
26
27 --------------------------------
28 -- Holes
29 tcInfer,
30 matchExpectedListTy,
31 matchExpectedTyConApp,
32 matchExpectedAppTy,
33 matchExpectedFunTys,
34 matchExpectedFunKind,
35 matchActualFunTySigma, matchActualFunTysRho,
36
37 checkTyVarEq, checkTyFamEq, checkTypeEq
38
39 ) where
40
41 import GHC.Prelude
42
43 import GHC.Hs
44 import GHC.Core.TyCo.Rep
45 import GHC.Core.TyCo.Ppr( debugPprType )
46 import GHC.Tc.Utils.Concrete ( mkWpFun )
47 import GHC.Tc.Utils.Env
48 import GHC.Tc.Utils.Instantiate
49 import GHC.Tc.Utils.Monad
50 import GHC.Tc.Utils.TcMType
51 import GHC.Tc.Utils.TcType
52
53
54 import GHC.Core.Type
55 import GHC.Core.Coercion
56 import GHC.Core.Multiplicity
57
58 import GHC.Tc.Types.Evidence
59 import GHC.Tc.Types.Constraint
60 import GHC.Tc.Types.Origin
61 import GHC.Types.Name( isSystemName )
62
63 import GHC.Core.TyCon
64 import GHC.Builtin.Types
65 import GHC.Types.Var as Var
66 import GHC.Types.Var.Set
67 import GHC.Types.Var.Env
68 import GHC.Utils.Error
69 import GHC.Driver.Session
70 import GHC.Types.Basic
71 import GHC.Data.Bag
72 import GHC.Utils.Misc
73 import GHC.Utils.Outputable as Outputable
74 import GHC.Utils.Panic
75 import GHC.Utils.Panic.Plain
76
77 import GHC.Exts ( inline )
78 import Control.Monad
79 import Control.Arrow ( second )
80 import qualified Data.Semigroup as S ( (<>) )
81
82 {- *********************************************************************
83 * *
84 matchActualFunTys
85 * *
86 ********************************************************************* -}
87
88 -- | matchActualFunTySigma does looks for just one function arrow
89 -- returning an uninstantiated sigma-type
90 matchActualFunTySigma
91 :: SDoc -- See Note [Herald for matchExpectedFunTys]
92 -> Maybe SDoc -- The thing with type TcSigmaType
93 -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and
94 -- types of values args to which function has
95 -- been applied already (reversed)
96 -- Both are used only for error messages)
97 -> TcRhoType -- Type to analyse: a TcRhoType
98 -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
99 -- The /argument/ is a RhoType
100 -- The /result/ is an (uninstantiated) SigmaType
101 --
102 -- See Note [matchActualFunTy error handling] for the first three arguments
103
104 -- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty
105 -- then wrap :: fun_ty ~> (arg_ty -> res_ty)
106 -- and NB: res_ty is an (uninstantiated) SigmaType
107
108 matchActualFunTySigma herald mb_thing err_info fun_ty
109 = assertPpr (isRhoTy fun_ty) (ppr fun_ty) $
110 go fun_ty
111 where
112 -- Does not allocate unnecessary meta variables: if the input already is
113 -- a function, we just take it apart. Not only is this efficient,
114 -- it's important for higher rank: the argument might be of form
115 -- (forall a. ty) -> other
116 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
117 -- hide the forall inside a meta-variable
118 go :: TcRhoType -- The type we're processing, perhaps after
119 -- expanding any type synonym
120 -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
121 go ty | Just ty' <- tcView ty = go ty'
122
123 go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
124 = assert (af == VisArg) $
125 return (idHsWrapper, Scaled w arg_ty, res_ty)
126
127 go ty@(TyVarTy tv)
128 | isMetaTyVar tv
129 = do { cts <- readMetaTyVar tv
130 ; case cts of
131 Indirect ty' -> go ty'
132 Flexi -> defer ty }
133
134 -- In all other cases we bale out into ordinary unification
135 -- However unlike the meta-tyvar case, we are sure that the
136 -- number of arguments doesn't match arity of the original
137 -- type, so we can add a bit more context to the error message
138 -- (cf #7869).
139 --
140 -- It is not always an error, because specialized type may have
141 -- different arity, for example:
142 --
143 -- > f1 = f2 'a'
144 -- > f2 :: Monad m => m Bool
145 -- > f2 = undefined
146 --
147 -- But in that case we add specialized type into error context
148 -- anyway, because it may be useful. See also #9605.
149 go ty = addErrCtxtM (mk_ctxt ty) (defer ty)
150
151 ------------
152 defer fun_ty
153 = do { arg_ty <- newOpenFlexiTyVarTy
154 ; res_ty <- newOpenFlexiTyVarTy
155 ; mult <- newFlexiTyVarTy multiplicityTy
156 ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty
157 ; co <- unifyType mb_thing fun_ty unif_fun_ty
158 ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
159
160 ------------
161 mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
162 mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far)
163 res_ty n_val_args_in_call
164 (n_val_args_in_call, arg_tys_so_far) = err_info
165
166 {- Note [matchActualFunTy error handling]
167 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
168 matchActualFunTySigma is made much more complicated by the
169 desire to produce good error messages. Consider the application
170 f @Int x y
171 In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
172 and then call matchActualFunTysPart for each individual value
173 argument. It, in turn, must instantiate any type/dictionary args,
174 before looking for an arrow type.
175
176 But if it doesn't find an arrow type, it wants to generate a message
177 like "f is applied to two arguments but its type only has one".
178 To do that, it needs to know about the args that tcArgs has already
179 munched up -- hence passing in n_val_args_in_call and arg_tys_so_far;
180 and hence also the accumulating so_far arg to 'go'.
181
182 This allows us (in mk_ctxt) to construct f's /instantiated/ type,
183 with just the values-arg arrows, which is what we really want
184 in the error message.
185
186 Ugh!
187 -}
188
189 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
190 -- for example in function application
191 matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys]
192 -> CtOrigin
193 -> Maybe SDoc -- the thing with type TcSigmaType
194 -> Arity
195 -> TcSigmaType
196 -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
197 -- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
198 -- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
199 -- and res_ty is a RhoType
200 -- NB: the returned type is top-instantiated; it's a RhoType
201 matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
202 = go n_val_args_wanted [] fun_ty
203 where
204 go n so_far fun_ty
205 | not (isRhoTy fun_ty)
206 = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty
207 ; (wrap2, arg_tys, res_ty) <- go n so_far rho
208 ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
209
210 go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
211
212 go n so_far fun_ty
213 = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma
214 herald mb_thing
215 (n_val_args_wanted, so_far)
216 fun_ty
217 ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
218 ; wrap_fun2 <- mkWpFun idHsWrapper wrap_res arg_ty1 res_ty (WpFunFunTy fun_ty)
219 ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
220
221 {-
222 ************************************************************************
223 * *
224 matchExpected functions
225 * *
226 ************************************************************************
227
228 Note [Herald for matchExpectedFunTys]
229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
230 The 'herald' always looks like:
231 "The equation(s) for 'f' have"
232 "The abstraction (\x.e) takes"
233 "The section (+ x) expects"
234 "The function 'f' is applied to"
235
236 This is used to construct a message of form
237
238 The abstraction `\Just 1 -> ...' takes two arguments
239 but its type `Maybe a -> a' has only one
240
241 The equation(s) for `f' have two arguments
242 but its type `Maybe a -> a' has only one
243
244 The section `(f 3)' requires 'f' to take two arguments
245 but its type `Int -> Int' has only one
246
247 The function 'f' is applied to two arguments
248 but its type `Int -> Int' has only one
249
250 When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
251 picture, we have a choice in deciding whether to count the type applications as
252 proper arguments:
253
254 The function 'f' is applied to one visible type argument
255 and two value arguments
256 but its type `forall a. a -> a` has only one visible type argument
257 and one value argument
258
259 Or whether to include the type applications as part of the herald itself:
260
261 The expression 'f @Int' is applied to two arguments
262 but its type `Int -> Int` has only one
263
264 The latter is easier to implement and is arguably easier to understand, so we
265 choose to implement that option.
266
267 Note [matchExpectedFunTys]
268 ~~~~~~~~~~~~~~~~~~~~~~~~~~
269 matchExpectedFunTys checks that a sigma has the form
270 of an n-ary function. It passes the decomposed type to the
271 thing_inside, and returns a wrapper to coerce between the two types
272
273 It's used wherever a language construct must have a functional type,
274 namely:
275 A lambda expression
276 A function definition
277 An operator section
278
279 This function must be written CPS'd because it needs to fill in the
280 ExpTypes produced for arguments before it can fill in the ExpType
281 passed in.
282
283 -}
284
285 -- Use this one when you have an "expected" type.
286 -- This function skolemises at each polytype.
287 matchExpectedFunTys :: forall a.
288 SDoc -- See Note [Herald for matchExpectedFunTys]
289 -> UserTypeCtxt
290 -> Arity
291 -> ExpRhoType -- Skolemised
292 -> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a)
293 -> TcM (HsWrapper, a)
294 -- If matchExpectedFunTys n ty = (_, wrap)
295 -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
296 -- where [t1, ..., tn], ty_r are passed to the thing_inside
297 matchExpectedFunTys herald ctx arity orig_ty thing_inside
298 = case orig_ty of
299 Check ty -> go [] arity ty
300 _ -> defer [] arity orig_ty
301 where
302 -- Skolemise any foralls /before/ the zero-arg case
303 -- so that we guarantee to return a rho-type
304 go acc_arg_tys n ty
305 | (tvs, theta, _) <- tcSplitSigmaTy ty
306 , not (null tvs && null theta)
307 = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' ->
308 go acc_arg_tys n ty'
309 ; return (wrap_gen <.> wrap_res, result) }
310
311 -- No more args; do this /before/ tcView, so
312 -- that we do not unnecessarily unwrap synonyms
313 go acc_arg_tys 0 rho_ty
314 = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty)
315 ; return (idHsWrapper, result) }
316
317 go acc_arg_tys n ty
318 | Just ty' <- tcView ty = go acc_arg_tys n ty'
319
320 go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
321 = assert (af == VisArg) $
322 do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
323 (n-1) res_ty
324 ; fun_wrap <- mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty (WpFunFunExpTy orig_ty)
325 ; return ( fun_wrap, result ) }
326
327 go acc_arg_tys n ty@(TyVarTy tv)
328 | isMetaTyVar tv
329 = do { cts <- readMetaTyVar tv
330 ; case cts of
331 Indirect ty' -> go acc_arg_tys n ty'
332 Flexi -> defer acc_arg_tys n (mkCheckExpType ty) }
333
334 -- In all other cases we bale out into ordinary unification
335 -- However unlike the meta-tyvar case, we are sure that the
336 -- number of arguments doesn't match arity of the original
337 -- type, so we can add a bit more context to the error message
338 -- (cf #7869).
339 --
340 -- It is not always an error, because specialized type may have
341 -- different arity, for example:
342 --
343 -- > f1 = f2 'a'
344 -- > f2 :: Monad m => m Bool
345 -- > f2 = undefined
346 --
347 -- But in that case we add specialized type into error context
348 -- anyway, because it may be useful. See also #9605.
349 go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
350 defer acc_arg_tys n (mkCheckExpType ty)
351
352 ------------
353 defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
354 defer acc_arg_tys n fun_ty
355 = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType)
356 ; res_ty <- newInferExpType
357 ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
358 ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
359 ; res_ty <- readExpType res_ty
360 ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
361 ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
362 -- Not a good origin at all :-(
363 ; return (wrap, result) }
364
365 ------------
366 mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
367 mk_ctxt arg_tys res_ty env
368 = mkFunTysMsg env herald arg_tys' res_ty arity
369 where
370 arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $
371 reverse arg_tys
372 -- this is safe b/c we're called from "go"
373
374 mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity
375 -> TcM (TidyEnv, SDoc)
376 mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
377 = do { (env', fun_rho) <- zonkTidyTcType env $
378 mkVisFunTys arg_tys res_ty
379
380 ; let (all_arg_tys, _) = splitFunTys fun_rho
381 n_fun_args = length all_arg_tys
382
383 msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end
384 = text "In the result of a function call"
385 | otherwise
386 = hang (full_herald <> comma)
387 2 (sep [ text "but its type" <+> quotes (pprType fun_rho)
388 , if n_fun_args == 0 then text "has none"
389 else text "has only" <+> speakN n_fun_args])
390
391 ; return (env', msg) }
392 where
393 full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument")
394
395 ----------------------
396 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
397 -- Special case for lists
398 matchExpectedListTy exp_ty
399 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
400 ; return (co, elt_ty) }
401
402 ---------------------
403 matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
404 -> TcRhoType -- orig_ty
405 -> TcM (TcCoercionN, -- T k1 k2 k3 a b c ~N orig_ty
406 [TcSigmaType]) -- Element types, k1 k2 k3 a b c
407
408 -- It's used for wired-in tycons, so we call checkWiredInTyCon
409 -- Precondition: never called with FunTyCon
410 -- Precondition: input type :: *
411 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
412
413 matchExpectedTyConApp tc orig_ty
414 = assert (not $ isFunTyCon tc) $ go orig_ty
415 where
416 go ty
417 | Just ty' <- tcView ty
418 = go ty'
419
420 go ty@(TyConApp tycon args)
421 | tc == tycon -- Common case
422 = return (mkTcNomReflCo ty, args)
423
424 go (TyVarTy tv)
425 | isMetaTyVar tv
426 = do { cts <- readMetaTyVar tv
427 ; case cts of
428 Indirect ty -> go ty
429 Flexi -> defer }
430
431 go _ = defer
432
433 -- If the common case does not occur, instantiate a template
434 -- T k1 .. kn t1 .. tm, and unify with the original type
435 -- Doing it this way ensures that the types we return are
436 -- kind-compatible with T. For example, suppose we have
437 -- matchExpectedTyConApp T (f Maybe)
438 -- where data T a = MkT a
439 -- Then we don't want to instantiate T's data constructors with
440 -- (a::*) ~ Maybe
441 -- because that'll make types that are utterly ill-kinded.
442 -- This happened in #7368
443 defer
444 = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
445 ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
446 ; let args = mkTyVarTys arg_tvs
447 tc_template = mkTyConApp tc args
448 ; co <- unifyType Nothing tc_template orig_ty
449 ; return (co, args) }
450
451 ----------------------
452 matchExpectedAppTy :: TcRhoType -- orig_ty
453 -> TcM (TcCoercion, -- m a ~N orig_ty
454 (TcSigmaType, TcSigmaType)) -- Returns m, a
455 -- If the incoming type is a mutable type variable of kind k, then
456 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
457
458 matchExpectedAppTy orig_ty
459 = go orig_ty
460 where
461 go ty
462 | Just ty' <- tcView ty = go ty'
463
464 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
465 = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
466
467 go (TyVarTy tv)
468 | isMetaTyVar tv
469 = do { cts <- readMetaTyVar tv
470 ; case cts of
471 Indirect ty -> go ty
472 Flexi -> defer }
473
474 go _ = defer
475
476 -- Defer splitting by generating an equality constraint
477 defer
478 = do { ty1 <- newFlexiTyVarTy kind1
479 ; ty2 <- newFlexiTyVarTy kind2
480 ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
481 ; return (co, (ty1, ty2)) }
482
483 orig_kind = tcTypeKind orig_ty
484 kind1 = mkVisFunTyMany liftedTypeKind orig_kind
485 kind2 = liftedTypeKind -- m :: * -> k
486 -- arg type :: *
487
488 {-
489 ************************************************************************
490 * *
491 Subsumption checking
492 * *
493 ************************************************************************
494
495 Note [Subsumption checking: tcSubType]
496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
497 All the tcSubType calls have the form
498 tcSubType actual_ty expected_ty
499 which checks
500 actual_ty <= expected_ty
501
502 That is, that a value of type actual_ty is acceptable in
503 a place expecting a value of type expected_ty. I.e. that
504
505 actual ty is more polymorphic than expected_ty
506
507 It returns a wrapper function
508 co_fn :: actual_ty ~ expected_ty
509 which takes an HsExpr of type actual_ty into one of type
510 expected_ty.
511 -}
512
513
514 -----------------
515 -- tcWrapResult needs both un-type-checked (for origins and error messages)
516 -- and type-checked (for wrapping) expressions
517 tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
518 -> TcM (HsExpr GhcTc)
519 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
520
521 tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
522 -> TcM (HsExpr GhcTc)
523 tcWrapResultO orig rn_expr expr actual_ty res_ty
524 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
525 , text "Expected:" <+> ppr res_ty ])
526 ; wrap <- tcSubTypeNC orig GenSigCtxt (Just (ppr rn_expr)) actual_ty res_ty
527 ; return (mkHsWrap wrap expr) }
528
529 tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
530 -> TcRhoType -- Actual -- a rho-type not a sigma-type
531 -> ExpRhoType -- Expected
532 -> TcM (HsExpr GhcTc)
533 -- A version of tcWrapResult to use when the actual type is a
534 -- rho-type, so nothing to instantiate; just go straight to unify.
535 -- It means we don't need to pass in a CtOrigin
536 tcWrapResultMono rn_expr expr act_ty res_ty
537 = assertPpr (isRhoTy act_ty) (ppr act_ty $$ ppr rn_expr) $
538 do { co <- unifyExpectedType rn_expr act_ty res_ty
539 ; return (mkHsWrapCo co expr) }
540
541 unifyExpectedType :: HsExpr GhcRn
542 -> TcRhoType -- Actual -- a rho-type not a sigma-type
543 -> ExpRhoType -- Expected
544 -> TcM TcCoercionN
545 unifyExpectedType rn_expr act_ty exp_ty
546 = case exp_ty of
547 Infer inf_res -> fillInferResult act_ty inf_res
548 Check exp_ty -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
549
550 ------------------------
551 tcSubTypePat :: CtOrigin -> UserTypeCtxt
552 -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
553 -- Used in patterns; polarity is backwards compared
554 -- to tcSubType
555 -- If wrap = tc_sub_type_et t1 t2
556 -- => wrap :: t1 ~> t2
557 tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
558 = do { dflags <- getDynFlags
559 ; tc_sub_type dflags unifyTypeET inst_orig ctxt ty_actual ty_expected }
560
561 tcSubTypePat _ _ (Infer inf_res) ty_expected
562 = do { co <- fillInferResult ty_expected inf_res
563 -- In patterns we do not instantatiate
564
565 ; return (mkWpCastN (mkTcSymCo co)) }
566
567 ---------------
568 tcSubType :: CtOrigin -> UserTypeCtxt
569 -> TcSigmaType -- Actual
570 -> ExpRhoType -- Expected
571 -> TcM HsWrapper
572 -- Checks that 'actual' is more polymorphic than 'expected'
573 tcSubType orig ctxt ty_actual ty_expected
574 = addSubTypeCtxt ty_actual ty_expected $
575 do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
576 ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected }
577
578 tcSubTypeNC :: CtOrigin -- Used when instantiating
579 -> UserTypeCtxt -- Used when skolemising
580 -> Maybe SDoc -- The expression that has type 'actual' (if known)
581 -> TcSigmaType -- Actual type
582 -> ExpRhoType -- Expected type
583 -> TcM HsWrapper
584 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
585 = case res_ty of
586 Check ty_expected -> do { dflags <- getDynFlags
587 ; tc_sub_type dflags (unifyType m_thing) inst_orig ctxt
588 ty_actual ty_expected }
589
590 Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
591 -- See Note [Instantiation of InferResult]
592 ; co <- fillInferResult rho inf_res
593 ; return (mkWpCastN co <.> wrap) }
594
595 {- Note [Instantiation of InferResult]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 We now always instantiate before filling in InferResult, so that
598 the result is a TcRhoType: see #17173 for discussion.
599
600 For example:
601
602 1. Consider
603 f x = (*)
604 We want to instantiate the type of (*) before returning, else we
605 will infer the type
606 f :: forall {a}. a -> forall b. Num b => b -> b -> b
607 This is surely confusing for users.
608
609 And worse, the monomorphism restriction won't work properly. The MR is
610 dealt with in simplifyInfer, and simplifyInfer has no way of
611 instantiating. This could perhaps be worked around, but it may be
612 hard to know even when instantiation should happen.
613
614 2. Another reason. Consider
615 f :: (?x :: Int) => a -> a
616 g y = let ?x = 3::Int in f
617 Here want to instantiate f's type so that the ?x::Int constraint
618 gets discharged by the enclosing implicit-parameter binding.
619
620 3. Suppose one defines plus = (+). If we instantiate lazily, we will
621 infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
622 restriction compels us to infer
623 plus :: Integer -> Integer -> Integer
624 (or similar monotype). Indeed, the only way to know whether to apply
625 the monomorphism restriction at all is to instantiate
626
627 There is one place where we don't want to instantiate eagerly,
628 namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
629 command. See Note [Implementing :type] in GHC.Tc.Module.
630 -}
631
632 ---------------
633 tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
634 -- External entry point, but no ExpTypes on either side
635 -- Checks that actual <= expected
636 -- Returns HsWrapper :: actual ~ expected
637 tcSubTypeSigma ctxt ty_actual ty_expected
638 = do { dflags <- getDynFlags
639 ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected }
640 where
641 eq_orig = TypeEqOrigin { uo_actual = ty_actual
642 , uo_expected = ty_expected
643 , uo_thing = Nothing
644 , uo_visible = True }
645
646 ---------------
647 tc_sub_type :: DynFlags
648 -> (TcType -> TcType -> TcM TcCoercionN) -- How to unify
649 -> CtOrigin -- Used when instantiating
650 -> UserTypeCtxt -- Used when skolemising
651 -> TcSigmaType -- Actual; a sigma-type
652 -> TcSigmaType -- Expected; also a sigma-type
653 -> TcM HsWrapper
654 -- Checks that actual_ty is more polymorphic than expected_ty
655 -- If wrap = tc_sub_type t1 t2
656 -- => wrap :: t1 ~> t2
657 tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected
658 | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
659 , not (possibly_poly ty_actual)
660 = do { traceTc "tc_sub_type (drop to equality)" $
661 vcat [ text "ty_actual =" <+> ppr ty_actual
662 , text "ty_expected =" <+> ppr ty_expected ]
663 ; mkWpCastN <$>
664 unify ty_actual ty_expected }
665
666 | otherwise -- This is the general case
667 = do { traceTc "tc_sub_type (general case)" $
668 vcat [ text "ty_actual =" <+> ppr ty_actual
669 , text "ty_expected =" <+> ppr ty_expected ]
670
671 ; (sk_wrap, inner_wrap)
672 <- tcSkolemise ctxt ty_expected $ \ sk_rho ->
673 do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
674 ; cow <- unify rho_a sk_rho
675 ; return (mkWpCastN cow <.> wrap) }
676
677 ; return (sk_wrap <.> inner_wrap) }
678 where
679 possibly_poly ty = not (isRhoTy ty)
680
681 definitely_poly ty
682 | (tvs, theta, tau) <- tcSplitSigmaTy ty
683 , (tv:_) <- tvs
684 , null theta
685 , checkTyVarEq dflags tv tau `cterHasProblem` cteInsolubleOccurs
686 = True
687 | otherwise
688 = False
689
690 ------------------------
691 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
692 addSubTypeCtxt ty_actual ty_expected thing_inside
693 | isRhoTy ty_actual -- If there is no polymorphism involved, the
694 , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions)
695 = thing_inside -- gives enough context by itself
696 | otherwise
697 = addErrCtxtM mk_msg thing_inside
698 where
699 mk_msg tidy_env
700 = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual
701 -- might not be filled if we're debugging. ugh.
702 ; mb_ty_expected <- readExpType_maybe ty_expected
703 ; (tidy_env, ty_expected) <- case mb_ty_expected of
704 Just ty -> second mkCheckExpType <$>
705 zonkTidyTcType tidy_env ty
706 Nothing -> return (tidy_env, ty_expected)
707 ; ty_expected <- readExpType ty_expected
708 ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
709 ; let msg = vcat [ hang (text "When checking that:")
710 4 (ppr ty_actual)
711 , nest 2 (hang (text "is more polymorphic than:")
712 2 (ppr ty_expected)) ]
713 ; return (tidy_env, msg) }
714
715 {- Note [Don't skolemise unnecessarily]
716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
717 Suppose we are trying to solve
718 (Char->Char) <= (forall a. a->a)
719 We could skolemise the 'forall a', and then complain
720 that (Char ~ a) is insoluble; but that's a pretty obscure
721 error. It's better to say that
722 (Char->Char) ~ (forall a. a->a)
723 fails.
724
725 So roughly:
726 * if the ty_expected has an outermost forall
727 (i.e. skolemisation is the next thing we'd do)
728 * and the ty_actual has no top-level polymorphism (but looking deeply)
729 then we can revert to simple equality. But we need to be careful.
730 These examples are all fine:
731
732 * (Char->Char) <= (forall a. Char -> Char)
733 ty_expected isn't really polymorphic
734
735 * (Char->Char) <= (forall a. (a~Char) => a -> a)
736 ty_expected isn't really polymorphic
737
738 * (Char->Char) <= (forall a. F [a] Char -> Char)
739 where type instance F [x] t = t
740 ty_expected isn't really polymorphic
741
742 If we prematurely go to equality we'll reject a program we should
743 accept (e.g. #13752). So the test (which is only to improve
744 error message) is very conservative:
745 * ty_actual is /definitely/ monomorphic
746 * ty_expected is /definitely/ polymorphic
747
748 Note [Settting the argument context]
749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
750 Consider we are doing the ambiguity check for the (bogus)
751 f :: (forall a b. C b => a -> a) -> Int
752
753 We'll call
754 tcSubType ((forall a b. C b => a->a) -> Int )
755 ((forall a b. C b => a->a) -> Int )
756
757 with a UserTypeCtxt of (FunSigCtxt "f"). Then we'll do the co/contra thing
758 on the argument type of the (->) -- and at that point we want to switch
759 to a UserTypeCtxt of GenSigCtxt. Why?
760
761 * Error messages. If we stick with FunSigCtxt we get errors like
762 * Could not deduce: C b
763 from the context: C b0
764 bound by the type signature for:
765 f :: forall a b. C b => a->a
766 But of course f does not have that type signature!
767 Example tests: T10508, T7220a, Simple14
768
769 * Implications. We may decide to build an implication for the whole
770 ambiguity check, but we don't need one for each level within it,
771 and GHC.Tc.Utils.Unify.alwaysBuildImplication checks the UserTypeCtxt.
772 See Note [When to build an implication]
773
774 Note [Wrapper returned from tcSubMult]
775 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
776 There is no notion of multiplicity coercion in Core, therefore the wrapper
777 returned by tcSubMult (and derived functions such as tcCheckUsage and
778 checkManyPattern) is quite unlike any other wrapper: it checks whether the
779 coercion produced by the constraint solver is trivial, producing a type error
780 if it is not. This is implemented via the WpMultCoercion wrapper, as desugared
781 by GHC.HsToCore.Binds.dsHsWrapper, which does the reflexivity check.
782
783 This wrapper needs to be placed in the term; otherwise, checking of the
784 eventual coercion won't be triggered during desugaring. But it can be put
785 anywhere, since it doesn't affect the desugared code.
786
787 Why do we check this in the desugarer? It's a convenient place, since it's
788 right after all the constraints are solved. We need the constraints to be
789 solved to check whether they are trivial or not.
790
791 An alternative would be to have a kind of constraint which can
792 only produce trivial evidence. This would allow such checks to happen
793 in the constraint solver (#18756).
794 This would be similar to the existing setup for Concrete, see
795 Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete
796 (PHASE 1 in particular).
797 -}
798
799 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
800 tcSubMult origin w_actual w_expected
801 | Just (w1, w2) <- isMultMul w_actual =
802 do { w1 <- tcSubMult origin w1 w_expected
803 ; w2 <- tcSubMult origin w2 w_expected
804 ; return (w1 <.> w2) }
805 -- Currently, we consider p*q and sup p q to be equal. Therefore, p*q <= r is
806 -- equivalent to p <= r and q <= r. For other cases, we approximate p <= q by p
807 -- ~ q. This is not complete, but it's sound. See also Note [Overapproximating
808 -- multiplicities] in Multiplicity.
809 tcSubMult origin w_actual w_expected =
810 case submult w_actual w_expected of
811 Submult -> return WpHole
812 Unknown -> tcEqMult origin w_actual w_expected
813
814 tcEqMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
815 tcEqMult origin w_actual w_expected = do
816 {
817 -- Note that here we do not call to `submult`, so we check
818 -- for strict equality.
819 ; coercion <- uType TypeLevel origin w_actual w_expected
820 ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
821
822
823 {- *********************************************************************
824 * *
825 Generalisation
826 * *
827 ********************************************************************* -}
828
829 {- Note [Skolemisation]
830 ~~~~~~~~~~~~~~~~~~~~~~~
831 tcSkolemise takes "expected type" and strip off quantifiers to expose the
832 type underneath, binding the new skolems for the 'thing_inside'
833 The returned 'HsWrapper' has type (specific_ty -> expected_ty).
834
835 Note that for a nested type like
836 forall a. Eq a => forall b. Ord b => blah
837 we still only build one implication constraint
838 forall a b. (Eq a, Ord b) => <constraints>
839 This is just an optimisation, but it's why we use topSkolemise to
840 build the pieces from all the layers, before making a single call
841 to checkConstraints.
842
843 tcSkolemiseScoped is very similar, but differs in two ways:
844
845 * It deals specially with just the outer forall, bringing those type
846 variables into lexical scope. To my surprise, I found that doing
847 this unconditionally in tcSkolemise (i.e. doing it even if we don't
848 need to bring the variables into lexical scope, which is harmless)
849 caused a non-trivial (1%-ish) perf hit on the compiler.
850
851 * It always calls checkConstraints, even if there are no skolem
852 variables at all. Reason: there might be nested deferred errors
853 that must not be allowed to float to top level.
854 See Note [When to build an implication] below.
855 -}
856
857 tcSkolemise, tcSkolemiseScoped
858 :: UserTypeCtxt -> TcSigmaType
859 -> (TcType -> TcM result)
860 -> TcM (HsWrapper, result)
861 -- ^ The wrapper has type: spec_ty ~> expected_ty
862 -- See Note [Skolemisation] for the differences between
863 -- tcSkolemiseScoped and tcSkolemise
864
865 tcSkolemiseScoped ctxt expected_ty thing_inside
866 = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
867 ; let skol_tvs = map snd tv_prs
868 skol_info = SigSkol ctxt expected_ty tv_prs
869
870 ; (ev_binds, res)
871 <- checkConstraints skol_info skol_tvs given $
872 tcExtendNameTyVarEnv tv_prs $
873 thing_inside rho_ty
874
875 ; return (wrap <.> mkWpLet ev_binds, res) }
876
877 tcSkolemise ctxt expected_ty thing_inside
878 | isRhoTy expected_ty -- Short cut for common case
879 = do { res <- thing_inside expected_ty
880 ; return (idHsWrapper, res) }
881 | otherwise
882 = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
883
884 ; let skol_tvs = map snd tv_prs
885 skol_info = SigSkol ctxt expected_ty tv_prs
886
887 ; (ev_binds, result)
888 <- checkConstraints skol_info skol_tvs given $
889 thing_inside rho_ty
890
891 ; return (wrap <.> mkWpLet ev_binds, result) }
892 -- The ev_binds returned by checkConstraints is very
893 -- often empty, in which case mkWpLet is a no-op
894
895 -- | Variant of 'tcSkolemise' that takes an ExpType
896 tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
897 -> (ExpRhoType -> TcM result)
898 -> TcM (HsWrapper, result)
899 tcSkolemiseET _ et@(Infer {}) thing_inside
900 = (idHsWrapper, ) <$> thing_inside et
901 tcSkolemiseET ctxt (Check ty) thing_inside
902 = tcSkolemise ctxt ty $ \rho_ty ->
903 thing_inside (mkCheckExpType rho_ty)
904
905 checkConstraints :: SkolemInfo
906 -> [TcTyVar] -- Skolems
907 -> [EvVar] -- Given
908 -> TcM result
909 -> TcM (TcEvBinds, result)
910
911 checkConstraints skol_info skol_tvs given thing_inside
912 = do { implication_needed <- implicationNeeded skol_info skol_tvs given
913
914 ; if implication_needed
915 then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
916 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
917 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
918 ; emitImplications implics
919 ; return (ev_binds, result) }
920
921 else -- Fast path. We check every function argument with tcCheckPolyExpr,
922 -- which uses tcSkolemise and hence checkConstraints.
923 -- So this fast path is well-exercised
924 do { res <- thing_inside
925 ; return (emptyTcEvBinds, res) } }
926
927 checkTvConstraints :: SkolemInfo
928 -> [TcTyVar] -- Skolem tyvars
929 -> TcM result
930 -> TcM result
931
932 checkTvConstraints skol_info skol_tvs thing_inside
933 = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
934 ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
935 ; return result }
936
937 emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
938 -> TcLevel -> WantedConstraints -> TcM ()
939 emitResidualTvConstraint skol_info skol_tvs tclvl wanted
940 | not (isEmptyWC wanted) ||
941 checkTelescopeSkol skol_info
942 = -- checkTelescopeSkol: in this case, /always/ emit this implication
943 -- even if 'wanted' is empty. We need the implication so that we check
944 -- for a bad telescope. See Note [Skolem escape and forall-types] in
945 -- GHC.Tc.Gen.HsType
946 do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
947 ; emitImplication implic }
948
949 | otherwise -- Empty 'wanted', emit nothing
950 = return ()
951
952 buildTvImplication :: SkolemInfo -> [TcTyVar]
953 -> TcLevel -> WantedConstraints -> TcM Implication
954 buildTvImplication skol_info skol_tvs tclvl wanted
955 = do { ev_binds <- newNoTcEvBinds -- Used for equalities only, so all the constraints
956 -- are solved by filling in coercion holes, not
957 -- by creating a value-level evidence binding
958 ; implic <- newImplication
959
960 ; return (implic { ic_tclvl = tclvl
961 , ic_skols = skol_tvs
962 , ic_given_eqs = NoGivenEqs
963 , ic_wanted = wanted
964 , ic_binds = ev_binds
965 , ic_info = skol_info }) }
966
967 implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
968 -- See Note [When to build an implication]
969 implicationNeeded skol_info skol_tvs given
970 | null skol_tvs
971 , null given
972 , not (alwaysBuildImplication skol_info)
973 = -- Empty skolems and givens
974 do { tc_lvl <- getTcLevel
975 ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
976 then return False -- already inside an implication
977 else
978 do { dflags <- getDynFlags -- If any deferral can happen,
979 -- we must build an implication
980 ; return (gopt Opt_DeferTypeErrors dflags ||
981 gopt Opt_DeferTypedHoles dflags ||
982 gopt Opt_DeferOutOfScopeVariables dflags) } }
983
984 | otherwise -- Non-empty skolems or givens
985 = return True -- Definitely need an implication
986
987 alwaysBuildImplication :: SkolemInfo -> Bool
988 -- See Note [When to build an implication]
989 alwaysBuildImplication _ = False
990
991 {- Commmented out for now while I figure out about error messages.
992 See #14185
993
994 alwaysBuildImplication (SigSkol ctxt _ _)
995 = case ctxt of
996 FunSigCtxt {} -> True -- RHS of a binding with a signature
997 _ -> False
998 alwaysBuildImplication (RuleSkol {}) = True
999 alwaysBuildImplication (InstSkol {}) = True
1000 alwaysBuildImplication (FamInstSkol {}) = True
1001 alwaysBuildImplication _ = False
1002 -}
1003
1004 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
1005 -> [EvVar] -> WantedConstraints
1006 -> TcM (Bag Implication, TcEvBinds)
1007 buildImplicationFor tclvl skol_info skol_tvs given wanted
1008 | isEmptyWC wanted && null given
1009 -- Optimisation : if there are no wanteds, and no givens
1010 -- don't generate an implication at all.
1011 -- Reason for the (null given): we don't want to lose
1012 -- the "inaccessible alternative" error check
1013 = return (emptyBag, emptyTcEvBinds)
1014
1015 | otherwise
1016 = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
1017 -- Why allow TyVarTvs? Because implicitly declared kind variables in
1018 -- non-CUSK type declarations are TyVarTvs, and we need to bring them
1019 -- into scope as a skolem in an implication. This is OK, though,
1020 -- because TyVarTvs will always remain tyvars, even after unification.
1021 do { ev_binds_var <- newTcEvBinds
1022 ; implic <- newImplication
1023 ; let implic' = implic { ic_tclvl = tclvl
1024 , ic_skols = skol_tvs
1025 , ic_given = given
1026 , ic_wanted = wanted
1027 , ic_binds = ev_binds_var
1028 , ic_info = skol_info }
1029
1030 ; return (unitBag implic', TcEvBinds ev_binds_var) }
1031
1032 {- Note [When to build an implication]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1034 Suppose we have some 'skolems' and some 'givens', and we are
1035 considering whether to wrap the constraints in their scope into an
1036 implication. We must /always/ so if either 'skolems' or 'givens' are
1037 non-empty. But what if both are empty? You might think we could
1038 always drop the implication. Other things being equal, the fewer
1039 implications the better. Less clutter and overhead. But we must
1040 take care:
1041
1042 * If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
1043 we'll make a /term-level/ evidence binding for 'g = error "blah"'.
1044 We must have an EvBindsVar those bindings!, otherwise they end up as
1045 top-level unlifted bindings, which are verboten. This only matters
1046 at top level, so we check for that
1047 See also Note [Deferred errors for coercion holes] in GHC.Tc.Errors.
1048 cf #14149 for an example of what goes wrong.
1049
1050 * If you have
1051 f :: Int; f = f_blah
1052 g :: Bool; g = g_blah
1053 If we don't build an implication for f or g (no tyvars, no givens),
1054 the constraints for f_blah and g_blah are solved together. And that
1055 can yield /very/ confusing error messages, because we can get
1056 [W] C Int b1 -- from f_blah
1057 [W] C Int b2 -- from g_blan
1058 and fundpes can yield [D] b1 ~ b2, even though the two functions have
1059 literally nothing to do with each other. #14185 is an example.
1060 Building an implication keeps them separate.
1061 -}
1062
1063 {-
1064 ************************************************************************
1065 * *
1066 Boxy unification
1067 * *
1068 ************************************************************************
1069
1070 The exported functions are all defined as versions of some
1071 non-exported generic functions.
1072 -}
1073
1074 unifyType :: Maybe SDoc -- ^ If present, the thing that has type ty1
1075 -> TcTauType -> TcTauType -- ty1, ty2
1076 -> TcM TcCoercionN -- :: ty1 ~# ty2
1077 -- Actual and expected types
1078 -- Returns a coercion : ty1 ~ ty2
1079 unifyType thing ty1 ty2
1080 = uType TypeLevel origin ty1 ty2
1081 where
1082 origin = TypeEqOrigin { uo_actual = ty1
1083 , uo_expected = ty2
1084 , uo_thing = ppr <$> thing
1085 , uo_visible = True }
1086
1087 unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
1088 -- Like unifyType, but swap expected and actual in error messages
1089 -- This is used when typechecking patterns
1090 unifyTypeET ty1 ty2
1091 = uType TypeLevel origin ty1 ty2
1092 where
1093 origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped
1094 , uo_expected = ty1 -- NB swapped
1095 , uo_thing = Nothing
1096 , uo_visible = True }
1097
1098
1099 unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN
1100 unifyKind mb_thing ty1 ty2
1101 = uType KindLevel origin ty1 ty2
1102 where
1103 origin = TypeEqOrigin { uo_actual = ty1
1104 , uo_expected = ty2
1105 , uo_thing = mb_thing
1106 , uo_visible = True }
1107
1108
1109 {-
1110 %************************************************************************
1111 %* *
1112 uType and friends
1113 %* *
1114 %************************************************************************
1115
1116 uType is the heart of the unifier.
1117 -}
1118
1119 uType, uType_defer
1120 :: TypeOrKind
1121 -> CtOrigin
1122 -> TcType -- ty1 is the *actual* type
1123 -> TcType -- ty2 is the *expected* type
1124 -> TcM CoercionN
1125
1126 --------------
1127 -- It is always safe to defer unification to the main constraint solver
1128 -- See Note [Deferred unification]
1129 uType_defer t_or_k origin ty1 ty2
1130 = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
1131
1132 -- Error trace only
1133 -- NB. do *not* call mkErrInfo unless tracing is on,
1134 -- because it is hugely expensive (#5631)
1135 ; whenDOptM Opt_D_dump_tc_trace $ do
1136 { ctxt <- getErrCtxt
1137 ; doc <- mkErrInfo emptyTidyEnv ctxt
1138 ; traceTc "utype_defer" (vcat [ debugPprType ty1
1139 , debugPprType ty2
1140 , pprCtOrigin origin
1141 , doc])
1142 ; traceTc "utype_defer2" (ppr co)
1143 }
1144 ; return co }
1145
1146 --------------
1147 uType t_or_k origin orig_ty1 orig_ty2
1148 = do { tclvl <- getTcLevel
1149 ; traceTc "u_tys" $ vcat
1150 [ text "tclvl" <+> ppr tclvl
1151 , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
1152 , pprCtOrigin origin]
1153 ; co <- go orig_ty1 orig_ty2
1154 ; if isReflCo co
1155 then traceTc "u_tys yields no coercion" Outputable.empty
1156 else traceTc "u_tys yields coercion:" (ppr co)
1157 ; return co }
1158 where
1159 go :: TcType -> TcType -> TcM CoercionN
1160 -- The arguments to 'go' are always semantically identical
1161 -- to orig_ty{1,2} except for looking through type synonyms
1162
1163 -- Unwrap casts before looking for variables. This way, we can easily
1164 -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
1165 -- didn't do it this way, and then the unification above was deferred.
1166 go (CastTy t1 co1) t2
1167 = do { co_tys <- uType t_or_k origin t1 t2
1168 ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
1169
1170 go t1 (CastTy t2 co2)
1171 = do { co_tys <- uType t_or_k origin t1 t2
1172 ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
1173
1174 -- Variables; go for uUnfilledVar
1175 -- Note that we pass in *original* (before synonym expansion),
1176 -- so that type variables tend to get filled in with
1177 -- the most informative version of the type
1178 go (TyVarTy tv1) ty2
1179 = do { lookup_res <- isFilledMetaTyVar_maybe tv1
1180 ; case lookup_res of
1181 Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
1182 ; go ty1 ty2 }
1183 Nothing -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
1184 go ty1 (TyVarTy tv2)
1185 = do { lookup_res <- isFilledMetaTyVar_maybe tv2
1186 ; case lookup_res of
1187 Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
1188 ; go ty1 ty2 }
1189 Nothing -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
1190
1191 -- See Note [Expanding synonyms during unification]
1192 go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
1193 | tc1 == tc2
1194 = return $ mkNomReflCo ty1
1195
1196 -- See Note [Expanding synonyms during unification]
1197 --
1198 -- Also NB that we recurse to 'go' so that we don't push a
1199 -- new item on the origin stack. As a result if we have
1200 -- type Foo = Int
1201 -- and we try to unify Foo ~ Bool
1202 -- we'll end up saying "can't match Foo with Bool"
1203 -- rather than "can't match "Int with Bool". See #4535.
1204 go ty1 ty2
1205 | Just ty1' <- tcView ty1 = go ty1' ty2
1206 | Just ty2' <- tcView ty2 = go ty1 ty2'
1207
1208 -- Functions (t1 -> t2) just check the two parts
1209 -- Do not attempt (c => t); just defer
1210 go (FunTy { ft_af = VisArg, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
1211 (FunTy { ft_af = VisArg, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
1212 = do { co_l <- uType t_or_k origin arg1 arg2
1213 ; co_r <- uType t_or_k origin res1 res2
1214 ; co_w <- uType t_or_k origin w1 w2
1215 ; return $ mkFunCo Nominal co_w co_l co_r }
1216
1217 -- Always defer if a type synonym family (type function)
1218 -- is involved. (Data families behave rigidly.)
1219 go ty1@(TyConApp tc1 _) ty2
1220 | isTypeFamilyTyCon tc1 = defer ty1 ty2
1221 go ty1 ty2@(TyConApp tc2 _)
1222 | isTypeFamilyTyCon tc2 = defer ty1 ty2
1223
1224 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1225 -- See Note [Mismatched type lists and application decomposition]
1226 | tc1 == tc2, equalLength tys1 tys2
1227 = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $
1228 do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
1229 ; return $ mkTyConAppCo Nominal tc1 cos }
1230 where
1231 origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
1232 (tcTyConVisibilities tc1)
1233
1234 go (LitTy m) ty@(LitTy n)
1235 | m == n
1236 = return $ mkNomReflCo ty
1237
1238 -- See Note [Care with type applications]
1239 -- Do not decompose FunTy against App;
1240 -- it's often a type error, so leave it for the constraint solver
1241 go (AppTy s1 t1) (AppTy s2 t2)
1242 = go_app (isNextArgVisible s1) s1 t1 s2 t2
1243
1244 go (AppTy s1 t1) (TyConApp tc2 ts2)
1245 | Just (ts2', t2') <- snocView ts2
1246 = assert (not (mustBeSaturated tc2)) $
1247 go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
1248
1249 go (TyConApp tc1 ts1) (AppTy s2 t2)
1250 | Just (ts1', t1') <- snocView ts1
1251 = assert (not (mustBeSaturated tc1)) $
1252 go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
1253
1254 go (CoercionTy co1) (CoercionTy co2)
1255 = do { let ty1 = coercionType co1
1256 ty2 = coercionType co2
1257 ; kco <- uType KindLevel
1258 (KindEqOrigin orig_ty1 orig_ty2 origin
1259 (Just t_or_k))
1260 ty1 ty2
1261 ; return $ mkProofIrrelCo Nominal kco co1 co2 }
1262
1263 -- Anything else fails
1264 -- E.g. unifying for-all types, which is relative unusual
1265 go ty1 ty2 = defer ty1 ty2
1266
1267 ------------------
1268 defer ty1 ty2 -- See Note [Check for equality before deferring]
1269 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
1270 | otherwise = uType_defer t_or_k origin ty1 ty2
1271
1272 ------------------
1273 go_app vis s1 t1 s2 t2
1274 = do { co_s <- uType t_or_k origin s1 s2
1275 ; let arg_origin
1276 | vis = origin
1277 | otherwise = toInvisibleOrigin origin
1278 ; co_t <- uType t_or_k arg_origin t1 t2
1279 ; return $ mkAppCo co_s co_t }
1280
1281 {- Note [Check for equality before deferring]
1282 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1283 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
1284 If ty involves a type function we may defer, which isn't very sensible.
1285 An egregious example of this was in test T9872a, which has a type signature
1286 Proxy :: Proxy (Solutions Cubes)
1287 Doing the ambiguity check on this signature generates the equality
1288 Solutions Cubes ~ Solutions Cubes
1289 and currently the constraint solver normalises both sides at vast cost.
1290 This little short-cut in 'defer' helps quite a bit.
1291
1292 Note [Care with type applications]
1293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1294 Note: type applications need a bit of care!
1295 They can match FunTy and TyConApp, so use splitAppTy_maybe
1296 NB: we've already dealt with type variables and Notes,
1297 so if one type is an App the other one jolly well better be too
1298
1299 Note [Mismatched type lists and application decomposition]
1300 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1301 When we find two TyConApps, you might think that the argument lists
1302 are guaranteed equal length. But they aren't. Consider matching
1303 w (T x) ~ Foo (T x y)
1304 We do match (w ~ Foo) first, but in some circumstances we simply create
1305 a deferred constraint; and then go ahead and match (T x ~ T x y).
1306 This came up in #3950.
1307
1308 So either
1309 (a) either we must check for identical argument kinds
1310 when decomposing applications,
1311
1312 (b) or we must be prepared for ill-kinded unification sub-problems
1313
1314 Currently we adopt (b) since it seems more robust -- no need to maintain
1315 a global invariant.
1316
1317 Note [Expanding synonyms during unification]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 We expand synonyms during unification, but:
1320 * We expand *after* the variable case so that we tend to unify
1321 variables with un-expanded type synonym. This just makes it
1322 more likely that the inferred types will mention type synonyms
1323 understandable to the user
1324
1325 * Similarly, we expand *after* the CastTy case, just in case the
1326 CastTy wraps a variable.
1327
1328 * We expand *before* the TyConApp case. For example, if we have
1329 type Phantom a = Int
1330 and are unifying
1331 Phantom Int ~ Phantom Char
1332 it is *wrong* to unify Int and Char.
1333
1334 * The problem case immediately above can happen only with arguments
1335 to the tycon. So we check for nullary tycons *before* expanding.
1336 This is particularly helpful when checking (* ~ *), because * is
1337 now a type synonym.
1338
1339 Note [Deferred unification]
1340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1341 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
1342 and yet its consistency is undetermined. Previously, there was no way to still
1343 make it consistent. So a mismatch error was issued.
1344
1345 Now these unifications are deferred until constraint simplification, where type
1346 family instances and given equations may (or may not) establish the consistency.
1347 Deferred unifications are of the form
1348 F ... ~ ...
1349 or x ~ ...
1350 where F is a type function and x is a type variable.
1351 E.g.
1352 id :: x ~ y => x -> y
1353 id e = e
1354
1355 involves the unification x = y. It is deferred until we bring into account the
1356 context x ~ y to establish that it holds.
1357
1358 If available, we defer original types (rather than those where closed type
1359 synonyms have already been expanded via tcCoreView). This is, as usual, to
1360 improve error messages.
1361
1362
1363 ************************************************************************
1364 * *
1365 uUnfilledVar and friends
1366 * *
1367 ************************************************************************
1368
1369 @uunfilledVar@ is called when at least one of the types being unified is a
1370 variable. It does {\em not} assume that the variable is a fixed point
1371 of the substitution; rather, notice that @uVar@ (defined below) nips
1372 back into @uTys@ if it turns out that the variable is already bound.
1373 -}
1374
1375 ----------
1376 uUnfilledVar :: CtOrigin
1377 -> TypeOrKind
1378 -> SwapFlag
1379 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
1380 -- definitely not a /filled/ meta-tyvar
1381 -> TcTauType -- Type 2
1382 -> TcM Coercion
1383 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
1384 -- It might be a skolem, or untouchable, or meta
1385
1386 uUnfilledVar origin t_or_k swapped tv1 ty2
1387 = do { ty2 <- zonkTcType ty2
1388 -- Zonk to expose things to the
1389 -- occurs check, and so that if ty2
1390 -- looks like a type variable then it
1391 -- /is/ a type variable
1392 ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
1393
1394 ----------
1395 uUnfilledVar1 :: CtOrigin
1396 -> TypeOrKind
1397 -> SwapFlag
1398 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
1399 -- definitely not a /filled/ meta-tyvar
1400 -> TcTauType -- Type 2, zonked
1401 -> TcM Coercion
1402 uUnfilledVar1 origin t_or_k swapped tv1 ty2
1403 | Just tv2 <- tcGetTyVar_maybe ty2
1404 = go tv2
1405
1406 | otherwise
1407 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1408
1409 where
1410 -- 'go' handles the case where both are
1411 -- tyvars so we might want to swap
1412 -- E.g. maybe tv2 is a meta-tyvar and tv1 is not
1413 go tv2 | tv1 == tv2 -- Same type variable => no-op
1414 = return (mkNomReflCo (mkTyVarTy tv1))
1415
1416 | swapOverTyVars False tv1 tv2 -- Distinct type variables
1417 -- Swap meta tyvar to the left if poss
1418 = do { tv1 <- zonkTyCoVarKind tv1
1419 -- We must zonk tv1's kind because that might
1420 -- not have happened yet, and it's an invariant of
1421 -- uUnfilledTyVar2 that ty2 is fully zonked
1422 -- Omitting this caused #16902
1423 ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
1424 tv2 (mkTyVarTy tv1) }
1425
1426 | otherwise
1427 = uUnfilledVar2 origin t_or_k swapped tv1 ty2
1428
1429 ----------
1430 uUnfilledVar2 :: CtOrigin
1431 -> TypeOrKind
1432 -> SwapFlag
1433 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
1434 -- definitely not a /filled/ meta-tyvar
1435 -> TcTauType -- Type 2, zonked
1436 -> TcM Coercion
1437 uUnfilledVar2 origin t_or_k swapped tv1 ty2
1438 = do { dflags <- getDynFlags
1439 ; cur_lvl <- getTcLevel
1440 ; go dflags cur_lvl }
1441 where
1442 go dflags cur_lvl
1443 | isTouchableMetaTyVar cur_lvl tv1
1444 -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
1445 , canSolveByUnification (metaTyVarInfo tv1) ty2
1446 , cterHasNoProblem (checkTyVarEq dflags tv1 ty2)
1447 -- See Note [Prevent unification with type families]
1448 = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
1449 ; traceTc "uUnfilledVar2 ok" $
1450 vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
1451 , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2)
1452 , ppr (isTcReflCo co_k), ppr co_k ]
1453
1454 ; if isTcReflCo co_k
1455 -- Only proceed if the kinds match
1456 -- NB: tv1 should still be unfilled, despite the kind unification
1457 -- because tv1 is not free in ty2 (or, hence, in its kind)
1458 then do { writeMetaTyVar tv1 ty2
1459 ; return (mkTcNomReflCo ty2) }
1460
1461 else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical
1462 -- Note [Equalities with incompatible kinds]
1463
1464 | otherwise
1465 = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
1466 -- Occurs check or an untouchable: just defer
1467 -- NB: occurs check isn't necessarily fatal:
1468 -- eg tv1 occurred in type family parameter
1469 ; defer }
1470
1471 ty1 = mkTyVarTy tv1
1472 kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
1473
1474 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
1475
1476 canSolveByUnification :: MetaInfo -> TcType -> Bool
1477 -- See Note [Unification preconditions, (TYVAR-TV)]
1478 canSolveByUnification info xi
1479 = case info of
1480 CycleBreakerTv -> False
1481 TyVarTv -> case tcGetTyVar_maybe xi of
1482 Nothing -> False
1483 Just tv -> case tcTyVarDetails tv of
1484 MetaTv { mtv_info = info }
1485 -> case info of
1486 TyVarTv -> True
1487 _ -> False
1488 SkolemTv {} -> True
1489 RuntimeUnk -> True
1490 _ -> True
1491
1492 swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
1493 swapOverTyVars is_given tv1 tv2
1494 -- See Note [Unification variables on the left]
1495 | not is_given, pri1 == 0, pri2 > 0 = True
1496 | not is_given, pri2 == 0, pri1 > 0 = False
1497
1498 -- Level comparison: see Note [TyVar/TyVar orientation]
1499 | lvl1 `strictlyDeeperThan` lvl2 = False
1500 | lvl2 `strictlyDeeperThan` lvl1 = True
1501
1502 -- Priority: see Note [TyVar/TyVar orientation]
1503 | pri1 > pri2 = False
1504 | pri2 > pri1 = True
1505
1506 -- Names: see Note [TyVar/TyVar orientation]
1507 | isSystemName tv2_name, not (isSystemName tv1_name) = True
1508
1509 | otherwise = False
1510
1511 where
1512 lvl1 = tcTyVarLevel tv1
1513 lvl2 = tcTyVarLevel tv2
1514 pri1 = lhsPriority tv1
1515 pri2 = lhsPriority tv2
1516 tv1_name = Var.varName tv1
1517 tv2_name = Var.varName tv2
1518
1519
1520 lhsPriority :: TcTyVar -> Int
1521 -- Higher => more important to be on the LHS
1522 -- => more likely to be eliminated
1523 -- See Note [TyVar/TyVar orientation]
1524 lhsPriority tv
1525 = assertPpr (isTyVar tv) (ppr tv) $
1526 case tcTyVarDetails tv of
1527 RuntimeUnk -> 0
1528 SkolemTv {} -> 0
1529 MetaTv { mtv_info = info } -> case info of
1530 CycleBreakerTv -> 0
1531 TyVarTv -> 1
1532 TauTv -> 2
1533 RuntimeUnkTv -> 3
1534
1535 {- Note [Unification preconditions]
1536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1537 Question: given a homogeneous equality (alpha ~# ty), when is it OK to
1538 unify alpha := ty?
1539
1540 This note only applied to /homogeneous/ equalities, in which both
1541 sides have the same kind.
1542
1543 There are three reasons not to unify:
1544
1545 1. (SKOL-ESC) Skolem-escape
1546 Consider the constraint
1547 forall[2] a[2]. alpha[1] ~ Maybe a[2]
1548 If we unify alpha := Maybe a, the skolem 'a' may escape its scope.
1549 The level alpha[1] says that alpha may be used outside this constraint,
1550 where 'a' is not in scope at all. So we must not unify.
1551
1552 Bottom line: when looking at a constraint alpha[n] := ty, do not unify
1553 if any free variable of 'ty' has level deeper (greater) than n
1554
1555 2. (UNTOUCHABLE) Untouchable unification variables
1556 Consider the constraint
1557 forall[2] a[2]. b[1] ~ Int => alpha[1] ~ Int
1558 There is no (SKOL-ESC) problem with unifying alpha := Int, but it might
1559 not be the principal solution. Perhaps the "right" solution is alpha := b.
1560 We simply can't tell. See "OutsideIn(X): modular type inference with local
1561 assumptions", section 2.2. We say that alpha[1] is "untouchable" inside
1562 this implication.
1563
1564 Bottom line: at amibient level 'l', when looking at a constraint
1565 alpha[n] ~ ty, do not unify alpha := ty if there are any given equalities
1566 between levels 'n' and 'l'.
1567
1568 Exactly what is a "given equality" for the purpose of (UNTOUCHABLE)?
1569 Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
1570
1571 3. (TYVAR-TV) Unifying TyVarTvs and CycleBreakerTvs
1572 This precondition looks at the MetaInfo of the unification variable:
1573
1574 * TyVarTv: When considering alpha{tyv} ~ ty, if alpha{tyv} is a
1575 TyVarTv it can only unify with a type variable, not with a
1576 structured type. So if 'ty' is a structured type, such as (Maybe x),
1577 don't unify.
1578
1579 * CycleBreakerTv: never unified, except by restoreTyVarCycles.
1580
1581
1582 Needless to say, all three have wrinkles:
1583
1584 * (SKOL-ESC) Promotion. Given alpha[n] ~ ty, what if beta[k] is free
1585 in 'ty', where beta is a unification variable, and k>n? 'beta'
1586 stands for a monotype, and since it is part of a level-n type
1587 (equal to alpha[n]), we must /promote/ beta to level n. Just make
1588 up a fresh gamma[n], and unify beta[k] := gamma[n].
1589
1590 * (TYVAR-TV) Unification variables. Suppose alpha[tyv,n] is a level-n
1591 TyVarTv (see Note [TyVarTv] in GHC.Tc.Types.TcMType)? Now
1592 consider alpha[tyv,n] ~ Bool. We don't want to unify because that
1593 would break the TyVarTv invariant.
1594
1595 What about alpha[tyv,n] ~ beta[tau,n], where beta is an ordinary
1596 TauTv? Again, don't unify, because beta might later be unified
1597 with, say Bool. (If levels permit, we reverse the orientation here;
1598 see Note [TyVar/TyVar orientation].)
1599
1600 * (UNTOUCHABLE) Untouchability. When considering (alpha[n] ~ ty), how
1601 do we know whether there are any given equalities between level n
1602 and the ambient level? We answer in two ways:
1603
1604 * In the eager unifier, we only unify if l=n. If not, alpha may be
1605 untouchable, and defer to the constraint solver. This check is
1606 made in GHC.Tc.Utils.uUnifilledVar2, in the guard
1607 isTouchableMetaTyVar.
1608
1609 * In the constraint solver, we track where Given equalities occur
1610 and use that to guard unification in GHC.Tc.Solver.Canonical.touchabilityTest
1611 More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
1612
1613 Historical note: in the olden days (pre 2021) the constraint solver
1614 also used to unify only if l=n. Equalities were "floated" out of the
1615 implication in a separate step, so that they would become touchable.
1616 But the float/don't-float question turned out to be very delicate,
1617 as you can see if you look at the long series of Notes associated with
1618 GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier
1619 to unify in-place, with no floating.
1620
1621 Note [TyVar/TyVar orientation]
1622 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1623 Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)?
1624 This is a surprisingly tricky question! This is invariant (TyEq:TV).
1625
1626 The question is answered by swapOverTyVars, which is used
1627 - in the eager unifier, in GHC.Tc.Utils.Unify.uUnfilledVar1
1628 - in the constraint solver, in GHC.Tc.Solver.Canonical.canEqCanLHS2
1629
1630 First note: only swap if you have to!
1631 See Note [Avoid unnecessary swaps]
1632
1633 So we look for a positive reason to swap, using a three-step test:
1634
1635 * Level comparison. If 'a' has deeper level than 'b',
1636 put 'a' on the left. See Note [Deeper level on the left]
1637
1638 * Priority. If the levels are the same, look at what kind of
1639 type variable it is, using 'lhsPriority'.
1640
1641 Generally speaking we always try to put a MetaTv on the left
1642 in preference to SkolemTv or RuntimeUnkTv:
1643 a) Because the MetaTv may be touchable and can be unified
1644 b) Even if it's not touchable, GHC.Tc.Solver.floatEqualities
1645 looks for meta tyvars on the left
1646
1647 Tie-breaking rules for MetaTvs:
1648 - CycleBreakerTv: This is essentially a stand-in for another type;
1649 it's untouchable and should have the same priority as a skolem: 0.
1650
1651 - TyVarTv: These can unify only with another tyvar, but we can't unify
1652 a TyVarTv with a TauTv, because then the TyVarTv could (transitively)
1653 get a non-tyvar type. So give these a low priority: 1.
1654
1655 - TauTv: This is the common case; we want these on the left so that they
1656 can be written to: 2.
1657
1658 - RuntimeUnkTv: These aren't really meta-variables used in type inference,
1659 but just a convenience in the implementation of the GHCi debugger.
1660 Eagerly write to these: 3. See Note [RuntimeUnkTv] in
1661 GHC.Runtime.Heap.Inspect.
1662
1663 * Names. If the level and priority comparisons are all
1664 equal, try to eliminate a TyVar with a System Name in
1665 favour of ones with a Name derived from a user type signature
1666
1667 * Age. At one point in the past we tried to break any remaining
1668 ties by eliminating the younger type variable, based on their
1669 Uniques. See Note [Eliminate younger unification variables]
1670 (which also explains why we don't do this any more)
1671
1672 Note [Unification variables on the left]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 For wanteds, but not givens, swap (skolem ~ meta-tv) regardless of
1675 level, so that the unification variable is on the left.
1676
1677 * We /don't/ want this for Givens because if we ave
1678 [G] a[2] ~ alpha[1]
1679 [W] Bool ~ a[2]
1680 we want to rewrite the wanted to Bool ~ alpha[1],
1681 so we can float the constraint and solve it.
1682
1683 * But for Wanteds putting the unification variable on
1684 the left means an easier job when floating, and when
1685 reporting errors -- just fewer cases to consider.
1686
1687 In particular, we get better skolem-escape messages:
1688 see #18114
1689
1690 Note [Deeper level on the left]
1691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1692 The most important thing is that we want to put tyvars with
1693 the deepest level on the left. The reason to do so differs for
1694 Wanteds and Givens, but either way, deepest wins! Simple.
1695
1696 * Wanteds. Putting the deepest variable on the left maximise the
1697 chances that it's a touchable meta-tyvar which can be solved.
1698
1699 * Givens. Suppose we have something like
1700 forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
1701
1702 If we orient the Given a[2] on the left, we'll rewrite the Wanted to
1703 (beta[1] ~ b[1]), and that can float out of the implication.
1704 Otherwise it can't. By putting the deepest variable on the left
1705 we maximise our changes of eliminating skolem capture.
1706
1707 See also GHC.Tc.Solver.InertSet Note [Let-bound skolems] for another reason
1708 to orient with the deepest skolem on the left.
1709
1710 IMPORTANT NOTE: this test does a level-number comparison on
1711 skolems, so it's important that skolems have (accurate) level
1712 numbers.
1713
1714 See #15009 for an further analysis of why "deepest on the left"
1715 is a good plan.
1716
1717 Note [Avoid unnecessary swaps]
1718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1719 If we swap without actually improving matters, we can get an infinite loop.
1720 Consider
1721 work item: a ~ b
1722 inert item: b ~ c
1723 We canonicalise the work-item to (a ~ c). If we then swap it before
1724 adding to the inert set, we'll add (c ~ a), and therefore kick out the
1725 inert guy, so we get
1726 new work item: b ~ c
1727 inert item: c ~ a
1728 And now the cycle just repeats
1729
1730 Historical Note [Eliminate younger unification variables]
1731 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1732 Given a choice of unifying
1733 alpha := beta or beta := alpha
1734 we try, if possible, to eliminate the "younger" one, as determined
1735 by `ltUnique`. Reason: the younger one is less likely to appear free in
1736 an existing inert constraint, and hence we are less likely to be forced
1737 into kicking out and rewriting inert constraints.
1738
1739 This is a performance optimisation only. It turns out to fix
1740 #14723 all by itself, but clearly not reliably so!
1741
1742 It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars).
1743 But, to my surprise, it didn't seem to make any significant difference
1744 to the compiler's performance, so I didn't take it any further. Still
1745 it seemed too nice to discard altogether, so I'm leaving these
1746 notes. SLPJ Jan 18.
1747
1748 Note [Prevent unification with type families]
1749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1750 We prevent unification with type families because of an uneasy compromise.
1751 It's perfectly sound to unify with type families, and it even improves the
1752 error messages in the testsuite. It also modestly improves performance, at
1753 least in some cases. But it's disastrous for test case perf/compiler/T3064.
1754 Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
1755 What do we do? Do we reduce F? Or do we use the given? Hard to know what's
1756 best. GHC reduces. This is a disaster for T3064, where the type's size
1757 spirals out of control during reduction. If we prevent
1758 unification with type families, then the solver happens to use the equality
1759 before expanding the type family.
1760
1761 It would be lovely in the future to revisit this problem and remove this
1762 extra, unnecessary check. But we retain it for now as it seems to work
1763 better in practice.
1764
1765 Revisited in Nov '20, along with removing flattening variables. Problem
1766 is still present, and the solution is still the same.
1767
1768 Note [Type synonyms and the occur check]
1769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1770 Generally speaking we try to update a variable with type synonyms not
1771 expanded, which improves later error messages, unless looking
1772 inside a type synonym may help resolve a spurious occurs check
1773 error. Consider:
1774 type A a = ()
1775
1776 f :: (A a -> a -> ()) -> ()
1777 f = \ _ -> ()
1778
1779 x :: ()
1780 x = f (\ x p -> p x)
1781
1782 We will eventually get a constraint of the form t ~ A t. The ok function above will
1783 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
1784 unified with the original type A t, we would lead the type checker into an infinite loop.
1785
1786 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
1787 the ok function expands the synonym to detect opportunities for occurs check success using
1788 the underlying definition of the type synonym.
1789
1790 The same applies later on in the constraint interaction code; see GHC.Tc.Solver.Interact,
1791 function @occ_check_ok@.
1792
1793 Note [Non-TcTyVars in GHC.Tc.Utils.Unify]
1794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1795 Because the same code is now shared between unifying types and unifying
1796 kinds, we sometimes will see proper TyVars floating around the unifier.
1797 Example (from test case polykinds/PolyKinds12):
1798
1799 type family Apply (f :: k1 -> k2) (x :: k1) :: k2
1800 type instance Apply g y = g y
1801
1802 When checking the instance declaration, we first *kind-check* the LHS
1803 and RHS, discovering that the instance really should be
1804
1805 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
1806
1807 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
1808 as a second pass, we desugar the RHS (which is done in functions prefixed
1809 with "tc" in GHC.Tc.TyCl"). By this time, all the kind-vars are proper
1810 TyVars, not TcTyVars, get some kind unification must happen.
1811
1812 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
1813 meta-tyvar.
1814
1815 This used to not be necessary for type-checking (that is, before * :: *)
1816 because expressions get desugared via an algorithm separate from
1817 type-checking (with wrappers, etc.). Types get desugared very differently,
1818 causing this wibble in behavior seen here.
1819 -}
1820
1821 -- | Breaks apart a function kind into its pieces.
1822 matchExpectedFunKind
1823 :: Outputable fun
1824 => fun -- ^ type, only for errors
1825 -> Arity -- ^ n: number of desired arrows
1826 -> TcKind -- ^ fun_ kind
1827 -> TcM Coercion -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
1828
1829 matchExpectedFunKind hs_ty n k = go n k
1830 where
1831 go 0 k = return (mkNomReflCo k)
1832
1833 go n k | Just k' <- tcView k = go n k'
1834
1835 go n k@(TyVarTy kvar)
1836 | isMetaTyVar kvar
1837 = do { maybe_kind <- readMetaTyVar kvar
1838 ; case maybe_kind of
1839 Indirect fun_kind -> go n fun_kind
1840 Flexi -> defer n k }
1841
1842 go n (FunTy { ft_mult = w, ft_arg = arg, ft_res = res })
1843 = do { co <- go (n-1) res
1844 ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) }
1845
1846 go n other
1847 = defer n other
1848
1849 defer n k
1850 = do { arg_kinds <- newMetaKindVars n
1851 ; res_kind <- newMetaKindVar
1852 ; let new_fun = mkVisFunTysMany arg_kinds res_kind
1853 origin = TypeEqOrigin { uo_actual = k
1854 , uo_expected = new_fun
1855 , uo_thing = Just (ppr hs_ty)
1856 , uo_visible = True
1857 }
1858 ; uType KindLevel origin k new_fun }
1859
1860 {- *********************************************************************
1861 * *
1862 Equality invariant checking
1863 * *
1864 ********************************************************************* -}
1865
1866
1867 {- Note [Checking for foralls]
1868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1869 Unless we have -XImpredicativeTypes (which is a totally unsupported
1870 feature), we do not want to unify
1871 alpha ~ (forall a. a->a) -> Int
1872 So we look for foralls hidden inside the type, and it's convenient
1873 to do that at the same time as the occurs check (which looks for
1874 occurrences of alpha).
1875
1876 However, it's not just a question of looking for foralls /anywhere/!
1877 Consider
1878 (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
1879 This is legal; e.g. dependent/should_compile/T11635.
1880
1881 We don't want to reject it because of the forall in beta's kind, but
1882 (see Note [Occurrence checking: look inside kinds] in GHC.Core.Type)
1883 we do need to look in beta's kind. So we carry a flag saying if a
1884 'forall' is OK, and switch the flag on when stepping inside a kind.
1885
1886 Why is it OK? Why does it not count as impredicative polymorphism?
1887 The reason foralls are bad is because we reply on "seeing" foralls
1888 when doing implicit instantiation. But the forall inside the kind is
1889 fine. We'll generate a kind equality constraint
1890 (forall k. k->*) ~ (forall k. k->*)
1891 to check that the kinds of lhs and rhs are compatible. If alpha's
1892 kind had instead been
1893 (alpha :: kappa)
1894 then this kind equality would rightly complain about unifying kappa
1895 with (forall k. k->*)
1896
1897 -}
1898
1899 ----------------
1900 {-# NOINLINE checkTyVarEq #-} -- checkTyVarEq becomes big after the `inline` fires
1901 checkTyVarEq :: DynFlags -> TcTyVar -> TcType -> CheckTyEqResult
1902 checkTyVarEq dflags tv ty
1903 = inline checkTypeEq dflags (TyVarLHS tv) ty
1904 -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
1905
1906 {-# NOINLINE checkTyFamEq #-} -- checkTyFamEq becomes big after the `inline` fires
1907 checkTyFamEq :: DynFlags
1908 -> TyCon -- type function
1909 -> [TcType] -- args, exactly saturated
1910 -> TcType -- RHS
1911 -> CheckTyEqResult -- always drops cteTypeFamily
1912 checkTyFamEq dflags fun_tc fun_args ty
1913 = inline checkTypeEq dflags (TyFamLHS fun_tc fun_args) ty
1914 `cterRemoveProblem` cteTypeFamily
1915 -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
1916
1917 checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
1918 -- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs
1919 -- is a canonical CEqCan.
1920 --
1921 -- In particular, this looks for:
1922 -- (a) a forall type (forall a. blah)
1923 -- (b) a predicate type (c => ty)
1924 -- (c) a type family; see Note [Prevent unification with type families]
1925 -- (d) a blocking coercion hole
1926 -- (e) an occurrence of the LHS (occurs check)
1927 --
1928 -- Note that an occurs-check does not mean "definite error". For example
1929 -- type family F a
1930 -- type instance F Int = Int
1931 -- consider
1932 -- b0 ~ F b0
1933 -- This is perfectly reasonable, if we later get b0 ~ Int. But we
1934 -- certainly can't unify b0 := F b0
1935 --
1936 -- For (a), (b), and (c) we check only the top level of the type, NOT
1937 -- inside the kinds of variables it mentions. For (d) we look deeply
1938 -- in coercions when the LHS is a tyvar (but skip coercions for type family
1939 -- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
1940 --
1941 -- checkTypeEq is called from
1942 -- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
1943 -- case-analysis on 'lhs')
1944 -- * checkEqCanLHSFinish, which does not know the form of 'lhs'
1945 checkTypeEq dflags lhs ty
1946 = go ty
1947 where
1948 impredicative = cteProblem cteImpredicative
1949 type_family = cteProblem cteTypeFamily
1950 hole_blocker = cteProblem cteHoleBlocker
1951 insoluble_occurs = cteProblem cteInsolubleOccurs
1952 soluble_occurs = cteProblem cteSolubleOccurs
1953
1954 -- The GHCi runtime debugger does its type-matching with
1955 -- unification variables that can unify with a polytype
1956 -- or a TyCon that would usually be disallowed by bad_tc
1957 -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect
1958 ghci_tv
1959 | TyVarLHS tv <- lhs
1960 , MetaTv { mtv_info = RuntimeUnkTv } <- tcTyVarDetails tv
1961 = True
1962
1963 | otherwise
1964 = False
1965
1966 go :: TcType -> CheckTyEqResult
1967 go (TyVarTy tv') = go_tv tv'
1968 go (TyConApp tc tys) = go_tc tc tys
1969 go (LitTy {}) = cteOK
1970 go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
1971 = go w S.<> go a S.<> go r S.<>
1972 if not ghci_tv && af == InvisArg
1973 then impredicative
1974 else cteOK
1975 go (AppTy fun arg) = go fun S.<> go arg
1976 go (CastTy ty co) = go ty S.<> go_co co
1977 go (CoercionTy co) = go_co co
1978 go (ForAllTy (Bndr tv' _) ty) = (case lhs of
1979 TyVarLHS tv | tv == tv' -> go_occ (tyVarKind tv') S.<> cterClearOccursCheck (go ty)
1980 | otherwise -> go_occ (tyVarKind tv') S.<> go ty
1981 _ -> go ty)
1982 S.<>
1983 if ghci_tv then cteOK else impredicative
1984
1985 go_tv :: TcTyVar -> CheckTyEqResult
1986 -- this slightly peculiar way of defining this means
1987 -- we don't have to evaluate this `case` at every variable
1988 -- occurrence
1989 go_tv = case lhs of
1990 TyVarLHS tv -> \ tv' -> go_occ (tyVarKind tv') S.<>
1991 if tv == tv' then insoluble_occurs else cteOK
1992 TyFamLHS {} -> \ _tv' -> cteOK
1993 -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type
1994
1995 -- For kinds, we only do an occurs check; we do not worry
1996 -- about type families or foralls
1997 -- See Note [Checking for foralls]
1998 go_occ k = cterFromKind $ go k
1999
2000 go_tc :: TyCon -> [TcType] -> CheckTyEqResult
2001 -- this slightly peculiar way of defining this means
2002 -- we don't have to evaluate this `case` at every tyconapp
2003 go_tc = case lhs of
2004 TyVarLHS {} -> \ tc tys -> check_tc tc S.<> go_tc_args tc tys
2005 TyFamLHS fam_tc fam_args -> \ tc tys ->
2006 if tcEqTyConApps fam_tc fam_args tc tys
2007 then insoluble_occurs
2008 else check_tc tc S.<> go_tc_args tc tys
2009
2010 -- just look at arguments, not the tycon itself
2011 go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult
2012 go_tc_args tc tys | isGenerativeTyCon tc Nominal = foldMap go tys
2013 | otherwise
2014 = let (tf_args, non_tf_args) = splitAt (tyConArity tc) tys in
2015 cterSetOccursCheckSoluble (foldMap go tf_args) S.<> foldMap go non_tf_args
2016
2017 -- no bother about impredicativity in coercions, as they're
2018 -- inferred
2019 go_co co | TyVarLHS tv <- lhs
2020 , tv `elemVarSet` tyCoVarsOfCo co
2021 = soluble_occurs S.<> maybe_hole_blocker
2022
2023 -- Don't check coercions for type families; see commentary at top of function
2024 | otherwise
2025 = maybe_hole_blocker
2026 where
2027 -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
2028 -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
2029 -- deferred type errors
2030 maybe_hole_blocker | not (gopt Opt_DeferTypeErrors dflags)
2031 , hasCoercionHoleCo co
2032 = hole_blocker
2033
2034 | otherwise
2035 = cteOK
2036
2037 check_tc :: TyCon -> CheckTyEqResult
2038 check_tc
2039 | ghci_tv = \ _tc -> cteOK
2040 | otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<>
2041 (if isFamFreeTyCon tc then cteOK else type_family)