Commit 0b89064c authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Make equality print better. (#11712)

parent 1701255c
......@@ -127,7 +127,8 @@ import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig
, DataCon, eqSpecTyVar )
import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
, tyCoVarsOfTypesWellScoped, varSetElemsWellScoped
, partitionInvisibles, coreView, typeKind )
, partitionInvisibles, coreView, typeKind
, eqType )
-- Transitively pulls in a LOT of stuff, better to break the loop
import {-# SOURCE #-} Coercion
......@@ -2772,6 +2773,9 @@ pprTcApp_help :: (a -> Type) -> TyPrec -> (TyPrec -> a -> SDoc)
-> TyCon -> [a] -> DynFlags -> PprStyle -> SDoc
-- This one has accss to the DynFlags
pprTcApp_help to_type p pp tc tys dflags style
| is_equality
= print_equality
| print_prefix
= pprPrefixApp p pp_tc (map (pp TyConPrec) tys_wo_kinds)
......@@ -2785,25 +2789,65 @@ pprTcApp_help to_type p pp tc tys dflags style
= pp_tc -- Do not wrap *, # in parens
| otherwise
= pprPrefixApp p (parens pp_tc) (map (pp TyConPrec) tys_wo_kinds)
= pprPrefixApp p (parens (pp_tc)) (map (pp TyConPrec) tys_wo_kinds)
where
tc_name = tyConName tc
-- With the solver working in unlifted equality, it will want to
-- to print unlifted equality constraints sometimes. But these are
-- confusing to users. So fix them up here.
(print_prefix, pp_tc)
| (tc `hasKey` eqPrimTyConKey || tc `hasKey` heqTyConKey) && not print_eqs
= (False, text "~")
| tc `hasKey` eqReprPrimTyConKey && not print_eqs
= (True, text "Coercible")
| otherwise
= (not (isSymOcc (nameOccName tc_name)), ppr tc)
print_eqs = gopt Opt_PrintEqualityRelations dflags ||
dumpStyle style ||
debugStyle style
is_equality = tc `hasKey` eqPrimTyConKey ||
tc `hasKey` heqTyConKey ||
tc `hasKey` eqReprPrimTyConKey ||
tc `hasKey` eqTyConKey
-- don't include Coercible here, which should be printed
-- normally
-- This is all a bit ad-hoc, trying to print out the best representation
-- of equalities. If you see a better design, go for it.
print_equality = case either_op_msg of
Left op ->
sep [ parens (pp TyOpPrec ty1 <+> dcolon <+> pp TyOpPrec ki1)
, op
, parens (pp TyOpPrec ty2 <+> dcolon <+> pp TyOpPrec ki2)]
Right msg ->
msg
where
hetero_tc = tc `hasKey` eqPrimTyConKey
|| tc `hasKey` eqReprPrimTyConKey
|| tc `hasKey` heqTyConKey
print_kinds = gopt Opt_PrintExplicitKinds dflags
print_eqs = gopt Opt_PrintEqualityRelations dflags ||
dumpStyle style ||
debugStyle style
(ki1, ki2, ty1, ty2)
| hetero_tc
, [k1, k2, t1, t2] <- tys
= (k1, k2, t1, t2)
| [k, t1, t2] <- tys -- we must have (~)
= (k, k, t1, t2)
| otherwise
= pprPanic "print_equality" pp_tc
-- if "Left", print hetero equality; if "Right" just print that msg
either_op_msg
| print_eqs
= Left pp_tc
| hetero_tc
, print_kinds || not (to_type ki1 `eqType` to_type ki2)
= Left $ if tc `hasKey` eqPrimTyConKey
then text "~~"
else pp_tc
| otherwise
= Right $ if tc `hasKey` eqReprPrimTyConKey
then text "Coercible" <+> (sep [ pp TyConPrec ty1
, pp TyConPrec ty2 ])
else sep [pp TyOpPrec ty1, text "~", pp TyOpPrec ty2]
print_prefix = not (isSymOcc (nameOccName tc_name))
tys_wo_kinds = suppressInvisibles to_type dflags tc tys
pp_tc = ppr tc
------------------
-- | Given a 'TyCon',and the args to which it is applied,
......
......@@ -10,9 +10,11 @@ T2431.$WRefl [InlPrag=INLINE] :: forall a. a :~: a
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=False,boring_ok=False)
Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)}]
Tmpl= \ (@ a) ->
T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))}]
T2431.$WRefl =
\ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)
\ (@ a) ->
T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))
-- RHS size: {terms: 4, types: 8, coercions: 0}
absurd :: forall a. Int :~: Bool -> a
......
......@@ -7,7 +7,7 @@ T7558.hs:8:4: error:
at T7558.hs:7:6
Inaccessible code in
a pattern with constructor:
MkT :: forall a b. (a ~ Maybe b) => a -> Maybe b -> T a b,
MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
in an equation for ‘f’
• In the pattern: MkT x y
In an equation for ‘f’: f (MkT x y) = [x, y] `seq` True
......
......@@ -90,13 +90,13 @@
Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
k :: (Int ~ Bool) => Int -> Bool
k :: Int ~ Bool => Int -> Bool
../../typecheck/should_run/Defer01.hs:45:6: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
k :: (Int ~ Bool) => Int -> Bool
k :: Int ~ Bool => Int -> Bool
• In the ambiguity check for ‘k’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
......
......@@ -4,7 +4,7 @@ PushedInAsGivens.hs:10:31: error:
because type variable ‘a1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
foo :: (F Int ~ [a1]) => a1 -> Int
foo :: F Int ~ [a1] => a1 -> Int
at PushedInAsGivens.hs:9:13-44
• In the expression: y
In the first argument of ‘length’, namely ‘[x, y]’
......
......@@ -4,11 +4,11 @@ Simple14.hs:8:8: error:
‘z0’ is untouchable
inside the constraints: x ~ y
bound by the type signature for:
eqE :: (x ~ y) => EQ_ z0 z0
eqE :: x ~ y => EQ_ z0 z0
at Simple14.hs:8:8-39
‘z’ is a rigid type variable bound by
the type signature for:
eqE :: forall x y z p. EQ_ x y -> ((x ~ y) => EQ_ z z) -> p
eqE :: forall x y z p. EQ_ x y -> (x ~ y => EQ_ z z) -> p
at Simple14.hs:8:8
Expected type: EQ_ z0 z0
Actual type: EQ_ z z
......
SimpleFail15.hs:5:8: error:
• Illegal qualified type: (a ~ b) => t
• Illegal qualified type: a ~ b => t
Perhaps you intended to use RankNTypes or Rank2Types
• In the type signature:
foo :: (a, b) -> (a ~ b => t) -> (a, b)
......@@ -3,11 +3,11 @@ T4093a.hs:8:8: error:
• Could not deduce: e ~ ()
from the context: Foo e ~ Maybe e
bound by the type signature for:
hang :: (Foo e ~ Maybe e) => Foo e
hang :: Foo e ~ Maybe e => Foo e
at T4093a.hs:7:1-34
‘e’ is a rigid type variable bound by
the type signature for:
hang :: forall e. (Foo e ~ Maybe e) => Foo e
hang :: forall e. Foo e ~ Maybe e => Foo e
at T4093a.hs:7:9
Expected type: Foo e
Actual type: Maybe ()
......
......@@ -3,11 +3,11 @@ TYPE SIGNATURES
DataFamilyInstanceLHS.B :: MyKind
DataFamilyInstanceLHS.SingA ::
forall (_ :: MyKind).
(_ ~ 'A) =>
_ ~ 'A =>
DataFamilyInstanceLHS.R:SingMyKind_ _
DataFamilyInstanceLHS.SingB ::
forall (_ :: MyKind).
(_ ~ 'B) =>
_ ~ 'B =>
DataFamilyInstanceLHS.R:SingMyKind_ _
foo :: Sing 'A
TYPE CONSTRUCTORS
......
......@@ -3,11 +3,11 @@ TYPE SIGNATURES
NamedWildcardInDataFamilyInstanceLHS.B :: MyKind
NamedWildcardInDataFamilyInstanceLHS.SingA ::
forall (_a :: MyKind).
(_a ~ 'A) =>
_a ~ 'A =>
NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a
NamedWildcardInDataFamilyInstanceLHS.SingB ::
forall (_a :: MyKind).
(_a ~ 'B) =>
_a ~ 'B =>
NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a
TYPE CONSTRUCTORS
data MyKind = A | B
......
......@@ -3,11 +3,11 @@ T10503.hs:8:6: error:
• Could not deduce: k ~ *
from the context: Proxy 'KProxy ~ Proxy 'KProxy
bound by the type signature for:
h :: (Proxy 'KProxy ~ Proxy 'KProxy) => r
h :: Proxy 'KProxy ~ Proxy 'KProxy => r
at T10503.hs:8:6-85
‘k’ is a rigid type variable bound by
the type signature for:
h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
h :: forall k r. (Proxy 'KProxy ~ Proxy 'KProxy => r) -> r
at T10503.hs:8:6
• In the ambiguity check for ‘h’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
......@@ -3,8 +3,7 @@ T7230.hs:48:32: error:
• Could not deduce: (x :<<= x1) ~ 'True
from the context: Increasing xs ~ 'True
bound by the type signature for:
crash :: (Increasing xs ~ 'True) =>
SList xs -> SBool (Increasing xs)
crash :: Increasing xs ~ 'True => SList xs -> SBool (Increasing xs)
at T7230.hs:47:1-68
or from: xs ~ (x : xs1)
bound by a pattern with constructor:
......@@ -19,7 +18,7 @@ T7230.hs:48:32: error:
in an equation for ‘crash’
at T7230.hs:48:17-26
Expected type: SBool (Increasing xs)
Actual type: SBool (x :<<= x1)
Actual type: SBool (x :<<= x1)
• In the expression: x %:<<= y
In an equation for ‘crash’:
crash (SCons x (SCons y xs)) = x %:<<= y
......
......@@ -4,12 +4,12 @@ T9222.hs:13:3: error:
‘b0’ is untouchable
inside the constraints: a ~ '(b0, c0)
bound by the type of the constructor ‘Want’:
(a ~ '(b0, c0)) => Proxy b0
a ~ '(b0, c0) => Proxy b0
at T9222.hs:13:3
‘b’ is a rigid type variable bound by
the type of the constructor ‘Want’:
forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
((a ~ '(b, c)) => Proxy b) -> Want a
(a ~ '(b, c) => Proxy b) -> Want a
at T9222.hs:13:3
Expected type: Proxy b0
Actual type: Proxy b
......
......@@ -13,7 +13,7 @@ convert :: Wrap Age -> Int
convert =
convert1
`cast` (<Wrap Age>_R -> Roles13.N:Wrap[0] Roles13.N:Age[0]
:: (Wrap Age -> Wrap Age) ~R# (Wrap Age -> Int))
:: ((Wrap Age -> Wrap Age) :: *) ~R# ((Wrap Age -> Int) :: *))
-- RHS size: {terms: 2, types: 0, coercions: 0}
$trModule1 :: GHC.Types.TrName
......
......@@ -23,7 +23,7 @@ TYPE CONSTRUCTORS
COERCION AXIOMS
axiom Roles3.N:C1 :: C1 a = a -> a -- Defined at Roles3.hs:6:1
axiom Roles3.N:C2 ::
C2 a b = (a ~ b) => a -> b -- Defined at Roles3.hs:9:1
C2 a b = a ~ b => a -> b -- Defined at Roles3.hs:9:1
axiom Roles3.N:C3 ::
C3 a b = a -> F3 b -> F3 b -- Defined at Roles3.hs:12:1
axiom Roles3.N:C4 ::
......
......@@ -2,7 +2,7 @@
FrozenErrorTests.hs:12:12: error:
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
a pattern with constructor: MkT3 :: forall a. (a ~ Bool) => T a,
a pattern with constructor: MkT3 :: forall a. a ~ Bool => T a,
in a case alternative
• In the pattern: MkT3
In a case alternative: MkT3 -> ()
......
T5858.hs:11:7: error:
Ambiguous type variables ‘t0’, ‘t1’ arising from a use of ‘infer’
prevents the constraint ‘(InferOverloaded
([t0], [t1]))’ from being solved.
Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
These potential instance exist:
instance (t1 ~ String) => InferOverloaded (t1, t1)
-- Defined at T5858.hs:8:10
In the expression: infer ([], [])
In an equation for ‘foo’: foo = infer ([], [])
Ambiguous type variables ‘t0’, ‘t1’ arising from a use of ‘infer’
prevents the constraint ‘(InferOverloaded
([t0], [t1]))’ from being solved.
Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
These potential instance exist:
instance t1 ~ String => InferOverloaded (t1, t1)
-- Defined at T5858.hs:8:10
In the expression: infer ([], [])
In an equation for ‘foo’: foo = infer ([], [])
......@@ -6,7 +6,7 @@ T7857.hs:8:11: error:
at T7857.hs:8:1-21
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance [safe] (a ~ ()) => PrintfType (IO a)
instance [safe] a ~ () => PrintfType (IO a)
-- Defined in ‘Text.Printf’
instance [safe] (PrintfArg a, PrintfType r) => PrintfType (a -> r)
-- Defined in ‘Text.Printf’
......
......@@ -3,7 +3,7 @@ T8392a.hs:6:8: error:
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
foo :: (Int ~ Bool) => a -> a
foo :: Int ~ Bool => a -> a
• In the ambiguity check for ‘foo’
In the type signature:
foo :: (Int ~ Bool) => a -> a
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment