Make equality print better. (#11712)
authorRichard Eisenberg <eir@cis.upenn.edu>
Fri, 18 Mar 2016 15:20:31 +0000 (11:20 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Mon, 21 Mar 2016 16:16:11 +0000 (12:16 -0400)
19 files changed:
compiler/types/TyCoRep.hs
testsuite/tests/deSugar/should_compile/T2431.stderr
testsuite/tests/gadt/T7558.stderr
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
testsuite/tests/indexed-types/should_compile/Simple14.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr
testsuite/tests/indexed-types/should_fail/T4093a.stderr
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
testsuite/tests/polykinds/T10503.stderr
testsuite/tests/polykinds/T7230.stderr
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/roles/should_compile/Roles13.stderr
testsuite/tests/roles/should_compile/Roles3.stderr
testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
testsuite/tests/typecheck/should_fail/T5858.stderr
testsuite/tests/typecheck/should_fail/T7857.stderr
testsuite/tests/typecheck/should_fail/T8392a.stderr

index 9a2036a..f2efb5f 100644 (file)
@@ -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,
index c3b23ff..63f13db 100644 (file)
@@ -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
index 5c610b2..6618346 100644 (file)
@@ -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
index 8591424..7318eb6 100644 (file)
     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:
index 37b1135..596b6e2 100644 (file)
@@ -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]’
index d0582b0..bbbe0fb 100644 (file)
@@ -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
index ef6b318..48d897d 100644 (file)
@@ -1,6 +1,6 @@
 
 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)
index 8f46170..d226122 100644 (file)
@@ -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 ()
index 7b12afc..476ee27 100644 (file)
@@ -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
index 5b8982b..cd20a9b 100644 (file)
@@ -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
index 141f16f..a74615c 100644 (file)
@@ -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
index 36e333c..0ca0310 100644 (file)
@@ -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
index b3d31ef..b3adf5b 100644 (file)
@@ -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
index e9b8f1a..8a92c12 100644 (file)
@@ -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
index ca496ed..5bf8034 100644 (file)
@@ -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 ::
index 6abb044..bff6ba5 100644 (file)
@@ -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 -> ()
index 7d974d8..08de488 100644 (file)
@@ -1,11 +1,11 @@
 
 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 ([], [])
index 2596efb..ef723a7 100644 (file)
@@ -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’
index ba2c5e4..df53c22 100644 (file)
@@ -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