[Git][ghc/ghc][wip/T23070-unify] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Apr 10 19:30:10 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
be54e3dc by Simon Peyton Jones at 2023-04-10T20:31:40+01:00
Wibbles
- - - - -
18 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/typecheck/should_compile/T13651.stderr
- testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
- testsuite/tests/typecheck/should_fail/T16512a.stderr
- testsuite/tests/typecheck/should_fail/T17139.hs
- testsuite/tests/typecheck/should_fail/T17139.stderr
- testsuite/tests/typecheck/should_fail/T18851c.stderr
- testsuite/tests/typecheck/should_fail/T21530a.stderr
- testsuite/tests/typecheck/should_fail/T7696.stderr
- testsuite/tests/typecheck/should_fail/T7869.stderr
- testsuite/tests/typecheck/should_fail/tcfail122.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -51,7 +51,7 @@ module GHC.Core.Coercion (
castCoercionKind, castCoercionKind1, castCoercionKind2,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
- mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+ mkNomPrimEqPred,
-- ** Decomposition
instNewTyCon_maybe,
@@ -2597,7 +2597,8 @@ mkCoercionType Phantom = \ty1 ty2 ->
in
TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
--- | Creates a primitive type equality predicate.
+-- | Creates a primitive nominal type equality predicate.
+-- t1 ~# t2
-- Invariant: the types are not Coercions
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred ty1 ty2
@@ -2606,22 +2607,9 @@ mkPrimEqPred ty1 ty2
k1 = typeKind ty1
k2 = typeKind ty2
--- | Makes a lifted equality predicate at the given role
-mkPrimEqPredRole :: Role -> Type -> Type -> PredType
-mkPrimEqPredRole Nominal = mkPrimEqPred
-mkPrimEqPredRole Representational = mkReprPrimEqPred
-mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
-
--- | Creates a primitive type equality predicate with explicit kinds
-mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
-
--- | Creates a primitive representational type equality predicate
--- with explicit kinds
-mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroReprPrimEqPred k1 k2 ty1 ty2
- = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
-
+-- | Creates a primitive representational type equality predicate.
+-- t1 ~R# t2
+-- Invariant: the types are not Coercions
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred ty1 ty2
= mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
@@ -2629,6 +2617,17 @@ mkReprPrimEqPred ty1 ty2
k1 = typeKind ty1
k2 = typeKind ty2
+-- | Makes a lifted equality predicate at the given role
+mkPrimEqPredRole :: Role -> Type -> Type -> PredType
+mkPrimEqPredRole Nominal = mkPrimEqPred
+mkPrimEqPredRole Representational = mkReprPrimEqPred
+mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
+
+-- | Creates a primitive nominal type equality predicate with an explicit
+-- (but homogeneous) kind: (~#) k k ty1 ty2
+mkNomPrimEqPred :: Kind -> Type -> Type -> Type
+mkNomPrimEqPred k ty1 ty2 = mkTyConApp eqPrimTyCon [k, k, ty1, ty2]
+
-- | Assuming that two types are the same, ignoring coercions, find
-- a nominal coercion between the types. This is useful when optimizing
-- transitivity over coercion applications, where splitting two
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Core.Predicate (
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
- mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+ mkNomPrimEqPred,
-- Class predicates
mkClassPred, isDictTy, typeDeterminesValue,
=====================================
compiler/GHC/HsToCore.hs
=====================================
@@ -764,7 +764,7 @@ mkUnsafeCoercePrimPair _old_id old_expr
unsafe_equality k a b
= ( mkTyApps (Var unsafe_equality_proof_id) [k,b,a]
, mkTyConApp unsafe_equality_tc [k,b,a]
- , mkHeteroPrimEqPred k k a b
+ , mkNomPrimEqPred k a b
)
-- NB: UnsafeRefl :: (b ~# a) -> UnsafeEquality a b, so we have to
-- carefully swap the arguments above
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -2921,6 +2921,18 @@ neededEvVars implic@(Implic { ic_given = givens
-------------------------------------------------
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
+-- Simplify any delayed errors: e.g. type and term holes
+-- NB: At this point we have finished with all the simple
+-- constraints; they are in wc_simple, not in the inert set.
+-- So those Wanteds will not rewrite these delayed errors.
+-- That's probably no bad thing.
+--
+-- However if we have [W] alpha ~ Maybe a, [W] alpha ~ Int
+-- and _ : alpha, then we'll /unify/ alpha with the first of
+-- the Wanteds we get, and thereby report (_ : Maybe a) or
+-- (_ : Int) unpredictably, depending on which we happen to see
+-- first. Doesn't matter much; there is a type error anyhow.
+-- T17139 is a case in point.
simplifyDelayedErrors = mapBagM simpl_err
where
simpl_err :: DelayedError -> TcS DelayedError
@@ -2937,6 +2949,7 @@ simplifyDelayedErrors = mapBagM simpl_err
-- code, because we have all the givens already set up
simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc })
= do { ty' <- rewriteType loc ty
+ ; traceTcS "simpl_hole" (ppr ty $$ ppr ty')
; return (h { hole_ty = ty' }) }
{- Note [Delete dead Given evidence bindings]
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -253,10 +253,12 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| Just can_eq_lhs1 <- canEqLHS_maybe ty1
- = canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2
+ = do { traceTcS "can_eq1" (ppr ty1 $$ ppr ty2)
+ ; canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 }
| Just can_eq_lhs2 <- canEqLHS_maybe ty2
- = canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1
+ = do { traceTcS "can_eq2" (ppr ty1 $$ ppr ty2)
+ ; canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1 }
-- If the type is TyConApp tc1 args1, then args1 really can't be less
-- than tyConArity tc1. It could be *more* than tyConArity, but then we
@@ -1414,7 +1416,7 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
= canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
| otherwise
- = canEqCanLHSHetero ev eq_rel swapped lhs1 k1 xi2 k2
+ = canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 k1 xi2 ps_xi2 k2
where
k1 = canEqLHSKind lhs1
@@ -1450,23 +1452,37 @@ But this sent solver in an infinite loop (see #19415).
-}
canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
+ -- (or reversed if SwapFlag=IsSwapped)
-> EqRel -> SwapFlag
- -> CanEqLHS -- xi1
+ -> CanEqLHS -> TcType -- xi1
-> TcKind -- ki1
- -> TcType -- xi2
+ -> TcType -> TcType -- xi2
-> TcKind -- ki2
-> TcS (StopOrContinue Ct)
-canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2
- -- See Note [Equalities with incompatible kinds]
- -- See Note [Kind Equality Orientation]
- -- NB: preserve left-to-right orientation!!
- -- See Note [Fundeps with instances, and equality orientation]
- -- wrinkle (W2) in GHC.Tc.Solver.Interact
- = do { (kind_ev, kind_co) <- mk_kind_eq -- :: ki1 ~N ki2
-
- ; let -- kind_co :: (ki1 :: *) ~N (ki2 :: *) (whether swapped or not)
- lhs_redn = mkReflRedn role xi1
- rhs_redn = mkGReflRightRedn role xi2 (mkSymCo kind_co)
+canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
+-- See Note [Equalities with incompatible kinds]
+-- See Note [Kind Equality Orientation]
+
+-- NB: preserve left-to-right orientation!! See wrinkle (W2) in
+-- Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Interact
+-- NotSwapped:
+-- ev :: (lhs1:ki1) ~r# (xi2:ki2)
+-- kind_co :: k11 ~# ki2 -- Same orientiation as ev
+-- type_ev :: lhs1 ~r# (xi2 |> sym kind_co)
+-- Swapped
+-- ev :: (xi2:ki2) ~r# (lhs1:ki1)
+-- kind_co :: ki2 ~# ki1 -- Same orientiation as ev
+-- type_ev :: (xi2 |> kind_co) ~r# lhs1
+
+ = do { (kind_co, start_again) <- mk_kind_eq -- :: ki1 ~N ki2
+ ; if start_again -- Successful unification, have another go
+ then startAgainWith (mkNonCanonical ev)
+ else
+ do { let lhs_redn = mkReflRedn role ps_xi1
+ rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co
+ mb_sym_kind_co = case swapped of
+ NotSwapped -> mkSymCo kind_co
+ IsSwapped -> kind_co
-- See Note [Equalities with incompatible kinds], Wrinkle (1)
-- This will be ignored in rewriteEqEvidence if the work item is a Given
@@ -1476,38 +1492,36 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2
(ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
- ; emitWorkNC [type_ev] -- delay the type equality until after we've finished
- -- the kind equality, which may unlock things
- -- See Note [Equalities with incompatible kinds]
+ ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co
+ ; canEqCanLHSHomo type_ev eq_rel swapped lhs1 ps_xi1 new_xi2 new_xi2 }}
- ; solveNonCanonicalEquality kind_ev NomEq ki1 ki2 }
where
- mk_kind_eq :: TcS (CtEvidence, CoercionN)
+ mk_kind_eq :: TcS (CoercionN, Bool)
+ -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped
+ -- Returned Bool = True if unifications happened, so we should retry
mk_kind_eq = case ev of
CtGiven { ctev_evar = evar }
- -> do { let kind_co = maybe_sym $ mkKindCo (mkCoVarCo evar) -- :: k1 ~ k2
- ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
- ; return (kind_ev, ctEvCoercion kind_ev) }
-
- CtWanted { ctev_rewriters = rewriters }
- -> newWantedEq kind_loc rewriters Nominal ki1 ki2
-
- xi1 = canEqLHSType lhs1
- loc = ctev_loc ev
- role = eqRelRole eq_rel
- kind_loc = mkKindLoc xi1 xi2 loc
- kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
-
- maybe_sym = case swapped of
- IsSwapped -> mkSymCo -- if the input is swapped, then we
- -- will have k2 ~ k1, so flip it to k1 ~ k2
- NotSwapped -> id
+ -> do { let kind_co = mkKindCo (mkCoVarCo evar)
+ pred_ty = unSwap swapped (mkNomPrimEqPred liftedTypeKind) ki1 ki2
+ kind_loc = mkKindLoc xi1 xi2 (ctev_loc ev)
+ ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
+ ; emitWorkNC [kind_ev]
+ ; return (ctEvCoercion kind_ev, False) }
+
+ CtWanted {}
+ -> do { (kind_co, unified) <- unifyWanteds ev Nominal $ \uenv ->
+ let uenv' = updUEnvLoc uenv (mkKindLoc xi1 xi2)
+ in unSwap swapped (uType uenv') ki1 ki2
+ ; return (kind_co, not (null unified)) }
+
+ xi1 = canEqLHSType lhs1
+ role = eqRelRole eq_rel
-canEqCanLHSHomo :: CtEvidence
+canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs
+ -- or, if swapped: rhs ~ lhs
-> EqRel -> SwapFlag
- -> CanEqLHS -- lhs (or, if swapped, rhs)
- -> TcType -- pretty lhs
- -> TcType -> TcType -- rhs, pretty rhs
+ -> CanEqLHS -> TcType -- lhs, pretty lhs
+ -> TcType -> TcType -- rhs, pretty rhs
-> TcS (StopOrContinue Ct)
-- Guaranteed that typeKind lhs == typeKind rhs
canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1988,7 +1988,7 @@ unifyFunDeps ev role do_unifications
fvs = tyCoVarsOfType (ctEvPred ev)
unifyWanteds :: CtEvidence -> Role
- -> (UnifyEnv -> TcM a)
+ -> (UnifyEnv -> TcM a) -- Some calls to uType
-> TcS (a, [TcTyVar])
-- Return coercions witnessing the equality of the two types,
-- emitting new work equalities where necessary to achieve that
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -205,7 +205,7 @@ module GHC.Tc.Utils.TcType (
---------------------------------
-- argument visibility
- tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
+ tyConVisibilities, isNextTyConArgVisible, isNextArgVisible
) where
@@ -2309,8 +2309,8 @@ Reason: the back end falls over with panic "primRepHint:VoidRep";
-- | For every arg a tycon can take, the returned list says True if the argument
-- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
-- allow for oversaturation.
-tcTyConVisibilities :: TyCon -> [Bool]
-tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
+tyConVisibilities :: TyCon -> [Bool]
+tyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
where
tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
tc_return_kind_viss = map isVisiblePiTyBinder (fst $ tcSplitPiTys (tyConResKind tc))
@@ -2318,7 +2318,7 @@ tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
-- | If the tycon is applied to the types, is the next argument visible?
isNextTyConArgVisible :: TyCon -> [Type] -> Bool
isNextTyConArgVisible tc tys
- = tcTyConVisibilities tc `getNth` length tys
+ = tyConVisibilities tc `getNth` length tys
-- | Should this type be applied to a visible argument?
-- E.g. (s t): is `t` a visible argument of `s`?
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1922,8 +1922,9 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
| tc1 == tc2, equalLength tys1 tys2
, isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
= assertPpr (isGenerativeTyCon tc1 role) (ppr tc1) $
- do { cos <- zipWith4M u_tc_arg (tyConBinders tc1)
- (tyConRoleListX role tc1)
+ do { traceTc "go-tycon" (ppr tc1 $$ ppr tys1 $$ ppr tys2 $$ ppr (take 10 (tyConRoleListX role tc1)))
+ ; cos <- zipWith4M u_tc_arg (tyConVisibilities tc1) -- Infinite
+ (tyConRoleListX role tc1) -- Infinite
tys1 tys2
; return $ mkTyConAppCo role tc1 cos }
@@ -1965,10 +1966,11 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
------------------
- u_tc_arg tc_bndr role ty1 ty2
- = uType env_arg ty1 ty2
+ u_tc_arg is_vis role ty1 ty2
+ = do { traceTc "u_tc_arg" (ppr role $$ ppr ty1 $$ ppr ty2)
+ ; uType env_arg ty1 ty2 }
where
- env_arg = env { u_loc = adjustCtLocTyConBinder tc_bndr (u_loc env)
+ env_arg = env { u_loc = adjustCtLoc is_vis False (u_loc env)
, u_role = role }
------------------
=====================================
testsuite/tests/typecheck/should_compile/T13651.stderr
=====================================
@@ -1,6 +1,6 @@
T13651.hs:12:8: error: [GHC-25897]
- • Could not deduce ‘cs ~ Bar (Foo h) (Foo s)’
+ • Could not deduce ‘cr ~ Bar h (Foo r)’
from the context: (F cr cu ~ Bar h (Bar r u),
F cu cs ~ Bar (Foo h) (Bar u s))
bound by the type signature for:
@@ -8,7 +8,7 @@ T13651.hs:12:8: error: [GHC-25897]
(F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
at T13651.hs:(12,8)-(14,65)
- ‘cs’ is a rigid type variable bound by
+ ‘cr’ is a rigid type variable bound by
the type signature for:
foo :: forall cr cu h r u cs s.
(F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
=====================================
testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
=====================================
@@ -1,20 +1,20 @@
AmbigFDs.hs:10:8: error: [GHC-25897]
- • Couldn't match type ‘b1’ with ‘b2’
+ • Couldn't match type ‘b2’ with ‘b1’
arising from a functional dependency between constraints:
- ‘C a b2’
+ ‘C a b1’
arising from a type ambiguity check for
the type signature for ‘foo’ at AmbigFDs.hs:10:8-35
- ‘C a b1’
+ ‘C a b2’
arising from the type signature for:
foo :: forall a b1 b2.
(C a b1, C a b2) =>
a -> Int at AmbigFDs.hs:10:8-35
- ‘b1’ is a rigid type variable bound by
+ ‘b2’ is a rigid type variable bound by
the type signature for:
foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
at AmbigFDs.hs:10:8-35
- ‘b2’ is a rigid type variable bound by
+ ‘b1’ is a rigid type variable bound by
the type signature for:
foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
at AmbigFDs.hs:10:8-35
=====================================
testsuite/tests/typecheck/should_fail/T16512a.stderr
=====================================
@@ -1,20 +1,18 @@
T16512a.hs:41:25: error: [GHC-25897]
- • Couldn't match type ‘as’ with ‘a : as’
+ • Couldn't match type ‘b’ with ‘a -> b’
Expected: AST (ListVariadic (a : as) b)
Actual: AST (ListVariadic as (a -> b))
- ‘as’ is a rigid type variable bound by
- a pattern with constructor:
- AnApplication :: forall (as :: [*]) b.
- AST (ListVariadic as b) -> ASTs as -> AnApplication b,
- in a case alternative
- at T16512a.hs:40:9-26
+ ‘b’ is a rigid type variable bound by
+ the type signature for:
+ unapply :: forall b. AST b -> AnApplication b
+ at T16512a.hs:37:1-35
• In the first argument of ‘AnApplication’, namely ‘g’
In the expression: AnApplication g (a `ConsAST` as)
In a case alternative:
AnApplication g as -> AnApplication g (a `ConsAST` as)
• Relevant bindings include
- as :: ASTs as (bound at T16512a.hs:40:25)
g :: AST (ListVariadic as (a -> b)) (bound at T16512a.hs:40:23)
a :: AST a (bound at T16512a.hs:38:15)
f :: AST (a -> b) (bound at T16512a.hs:38:10)
+ unapply :: AST b -> AnApplication b (bound at T16512a.hs:38:1)
=====================================
testsuite/tests/typecheck/should_fail/T17139.hs
=====================================
@@ -13,3 +13,46 @@ type family TypeFam f fun where
lift :: (a -> b) -> TypeFam f (a -> b)
lift f = \x -> _ (f <*> x)
+
+
+{-
+x :: alpha
+body of lambda :: beta
+
+[W] TypeFam f (a->b) ~ (alpha -> beta)
+-->
+[W] (f a -> TypeFam f b) ~ (alpha -> beta)
+-->
+ alpha := f a
+ beta := TypeFam f b
+
+(<*>) :: Applicative g => g (p -> q) -> g p -> g q
+
+f <*> x
+
+arg1
+ (a->b) ~ g0 (p0->q0)
+ g0 := ((->) a)
+ (p0 -> q0) ~ b <---------
+arg2
+ alpha ~ g0 p0
+ g0 ~ f <----------
+ p0 := a
+res
+ g0 q0
+
+Finish with
+ [W] f ~ (->) a
+ [W] b ~ (a -> q0)
+ --> rewrite b
+ [W] (a -> q0) ~ a -> (
+
+_ :: g0 q0 -> beta
+ :: (a -> q0) -> TypeFam f b
+ :: (a -> q0) -> TypeFam ((->) a) (a -> q0)
+ :: (a -> q0) -> (a->a) -> TypeFam (-> a) q0
+
+BUT we would get different error messages if we did
+ g0 := f
+and then encountered [W] g0 ~ ((->) a)
+-}
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_fail/T17139.stderr
=====================================
@@ -1,8 +1,8 @@
T17139.hs:15:16: error: [GHC-88464]
- • Found hole: _ :: (a -> b0) -> f a -> TypeFam f b0
+ • Found hole: _ :: (a -> b0) -> (a -> a) -> TypeFam ((->) a) b0
Where: ‘b0’ is an ambiguous type variable
- ‘a’, ‘f’ are rigid type variables bound by
+ ‘a’ is a rigid type variable bound by
the type signature for:
lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
at T17139.hs:14:1-38
=====================================
testsuite/tests/typecheck/should_fail/T18851c.stderr
=====================================
@@ -2,13 +2,13 @@
T18851c.hs:25:27: error: [GHC-25897]
• Could not deduce ‘n2 ~ n1’
arising from reasoning about an injective type family using constraints:
- ‘Plus1 n2 ~ n’
- arising from a type equality
- VSucc (Plus1 n2) ~ VSucc n at T18851c.hs:25:27-33
‘Plus1 n1 ~ n’
+ arising from a type equality
+ VSucc (Plus1 n1) ~ VSucc n at T18851c.hs:25:27-33
+ ‘Plus1 n2 ~ n’
arising from a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
- in an equation for ‘foo’ at T18851c.hs:25:6-12
+ in an equation for ‘foo’ at T18851c.hs:25:16-22
from the context: n ~ Plus1 n1
bound by a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
=====================================
testsuite/tests/typecheck/should_fail/T21530a.stderr
=====================================
@@ -1,6 +1,6 @@
T21530a.hs:14:7: error: [GHC-18872]
- • Couldn't match kind ‘Constraint’ with ‘*’
+ • Couldn't match kind ‘*’ with ‘Constraint’
When matching types
a0 :: *
Eq Int :: Constraint
=====================================
testsuite/tests/typecheck/should_fail/T7696.stderr
=====================================
@@ -1,6 +1,6 @@
T7696.hs:9:6: error: [GHC-18872]
- • Couldn't match kind ‘*’ with ‘* -> *’
+ • Couldn't match kind ‘* -> *’ with ‘*’
When matching types
t0 :: (* -> *) -> *
w :: * -> *
=====================================
testsuite/tests/typecheck/should_fail/T7869.stderr
=====================================
@@ -1,16 +1,18 @@
T7869.hs:3:12: error: [GHC-25897]
- • Couldn't match type ‘b1’ with ‘b’
+ • Couldn't match type ‘a1’ with ‘a’
Expected: [a1] -> b1
Actual: [a] -> b
- ‘b1’ is a rigid type variable bound by
+ ‘a1’ is a rigid type variable bound by
an expression type signature:
forall a1 b1. [a1] -> b1
at T7869.hs:3:20-27
- ‘b’ is a rigid type variable bound by
+ ‘a’ is a rigid type variable bound by
the inferred type of f :: [a] -> b
at T7869.hs:3:1-27
• In the expression: f x
In the expression: (\ x -> f x) :: [a] -> b
In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
- • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
+ • Relevant bindings include
+ x :: [a1] (bound at T7869.hs:3:7)
+ f :: [a] -> b (bound at T7869.hs:3:1)
=====================================
testsuite/tests/typecheck/should_fail/tcfail122.stderr
=====================================
@@ -1,6 +1,6 @@
tcfail122.hs:9:9: error: [GHC-18872]
- • Couldn't match kind ‘*’ with ‘* -> *’
+ • Couldn't match kind ‘* -> *’ with ‘*’
When matching types
c0 :: (* -> *) -> *
a :: * -> *
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be54e3dc369608143af483809271017749da6d14
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be54e3dc369608143af483809271017749da6d14
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230410/139aff18/attachment-0001.html>
More information about the ghc-commits
mailing list