Opened 2 months ago

Closed 5 weeks ago

#15039 closed bug (fixed)

Bizarre pretty-printing of inferred Coercible constraint in partial type signature

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.4.1
Keywords: PartialTypeSignatures, TypeInType Cc: partial-sigs/should_compile/T15039a, partial-sigs/should_compile/T15039b, partial-sigs/should_compile/T15039c, partial-sigs/should_compile/T15039d
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4696
Wiki Page:

Description

Consider the following GHCi session:

$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion

<interactive>:2:8: error:
    • Found type wildcard ‘_’
        standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
      Where: ‘a’, ‘b’ are rigid type variables bound by
               the inferred type of foo :: Coercible a b => Coercion a b
               at <interactive>:2:27-40
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: foo :: _ => Coercion a b
λ> :set -fprint-explicit-kinds 
λ> foo :: _ => Coercion a b; foo = Coercion

<interactive>:4:8: error:
    • Found type wildcard ‘_’
        standing for ‘(a :: *) ~~ (b :: *) :: TYPE
                                                ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
      Where: ‘a’, ‘b’ are rigid type variables bound by
               the inferred type of
                 foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
               at <interactive>:4:27-40
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: foo :: _ => Coercion a b

There are two things quite strange about this:

  1. In both error messages, GHC claims that Coercible a b/a ~~ b has kind TYPE (TupleRep '[]). This is wrong, and should be Coercible.
  2. For some reason, enabling -fprint-explicit-kinds causes the inferred constraint to be (~~) instead of Coercible, which is just plain wrong.

Change History (11)

comment:1 Changed 2 months ago by simonpj

I know what is going on here. When we first introduced explicit equalities Richard arranged to make the pretty-printer conceal some of the menagerie, with some ad-hoc rules sketched in IfaceType:

Note [Equality predicates in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC has several varieties of type equality (see Note [The equality types story]
in TysPrim for details).  In an effort to avoid confusing users, we suppress
the differences during "normal" pretty printing.  Specifically we display them
like this:

 Predicate                         Pretty-printed as
                          Homogeneous case        Heterogeneous case
 ----------------        -----------------        -------------------
 (~)    eqTyCon                 ~                  N/A
 (~~)   heqTyCon                ~                  ~~
 (~#)   eqPrimTyCon             ~#                 ~~
 (~R#)  eqReprPrimTyCon         Coercible          Coercible

By "homogeneeous case" we mean cases where a hetero-kinded equality
(all but the first above) is actually applied to two identical kinds.
Unfortunately, determining this from an IfaceType isn't possible since
we can't see through type synonyms. Consequently, we need to record
whether this particular application is homogeneous in IfaceTyConSort
for the purposes of pretty-printing.

All this suppresses information. To get the ground truth, use -dppr-debug
(see 'print_eqs' in 'ppr_equality').

See Note [The equality types story] in TysPrim.

There's a flag to control this: -fprint-equality-relations, and using that flag makes both oddities go away.

In this particular case, although it displays Coercible a b, it is really pretty printing a ~R# b! And that is why the kind looks wrong: it's the kind of a ~R# b. So concealing the reality is jolly confusing here.

Moreover, for reasons I don't understand, -fprint-explicit-kinds affects the behhaviour too, hence oddness (2).

It's all in IfaceType.ppr_equality, which I reproduce below

ppr_equality :: TyPrec -> IfaceTyCon -> [IfaceType] -> Maybe SDoc
ppr_equality ctxt_prec tc args
  | hetero_eq_tc
  , [k1, k2, t1, t2] <- args
  = Just $ print_equality (k1, k2, t1, t2)

  | hom_eq_tc
  , [k, t1, t2] <- args
  = Just $ print_equality (k, k, t1, t2)

  | otherwise
  = Nothing
  where
    homogeneous = case ifaceTyConSort $ ifaceTyConInfo tc of
                    IfaceEqualityTyCon -> True
                    _other             -> False
       -- True <=> a heterogeneous equality whose arguments
       --          are (in this case) of the same kind

    tc_name = ifaceTyConName tc
    pp = ppr_ty
    hom_eq_tc = tc_name `hasKey` eqTyConKey            -- (~)
    hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey     -- (~#)
                || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
                || tc_name `hasKey` heqTyConKey        -- (~~)
    print_equality args =
        sdocWithDynFlags $ \dflags ->
        getPprStyle      $ \style  ->
        print_equality' args style dflags

    print_equality' (ki1, ki2, ty1, ty2) style dflags
      | print_eqs   -- No magic, just print the original TyCon
      = ppr_infix_eq (ppr tc)

      | hetero_eq_tc
      , print_kinds || not homogeneous
      = ppr_infix_eq (text "~~")

      | otherwise
      = if tc_name `hasKey` eqReprPrimTyConKey
        then pprIfacePrefixApp ctxt_prec (text "Coercible")
                               [pp TyConPrec ty1, pp TyConPrec ty2]
        else pprIfaceInfixApp ctxt_prec (char '~')
                 (pp TyOpPrec ty1) (pp TyOpPrec ty2)
      where
        ppr_infix_eq eq_op
           = pprIfaceInfixApp ctxt_prec eq_op
                 (parens (pp TopPrec ty1 <+> dcolon <+> pp TyOpPrec ki1))
                 (parens (pp TopPrec ty2 <+> dcolon <+> pp TyOpPrec ki2))

        print_kinds = gopt Opt_PrintExplicitKinds dflags
        print_eqs   = gopt Opt_PrintEqualityRelations dflags ||
                      dumpStyle style || debugStyle style

What to do? I'm not sure. But that's what is going on.

Last edited 2 months ago by simonpj (previous) (diff)

comment:2 Changed 2 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 2 months ago by RyanGlScott

Well, that's one half of the mystery (2). Do you know why (1) is happening?

comment:4 Changed 2 months ago by goldfire

The idea is that, with -fprint-explicit-kinds, (a ~~ b) should be printed as ((a :: *) ~~ (b :: *)), with the explicit kinds. But (a ~# b) should also be printed as ((a :: *) ~~ (b :: *)), so as not to expose the user to ~#. Note that (a ~ b) is just printed as (a ~ b), even with -fprint-explicit-kinds, which seems wrong. And, of course, ~R# should never be printed with ~~.

What to do? Here are the cases. Assume a :: *, b :: *, and c :: k.

  1. Homogeneous equality a ~ b.
  1. Homogeneous use of heterogeneous equality a ~~ b.
  1. Heterogeneous use of heterogeneous equality a ~~ c.
  1. Homogeneous use of unlifted equality a ~# b.
  1. Heterogeneous use of unlifted equality a ~# c.
  1. Homegeneous representational equality Coercible a b.
  1. Homogeneous use of representational unlifted equality a ~#R b.
  1. Heterogeneous use of representational unlifted equality a ~R# c.

Note that there is no heterogeneous representational lifted equality (the counterpert to ~~). There could be, but there seems to be no use for it.

For each case, we must decide how to print

  1. By default
  2. With -fprint-explicit-kinds
  3. With -fprint-equality-relations
  4. With -fprint-explicit-kinds -fprint-equality-relations.

I propose:

    1. a ~ b
    2. (a :: *) ~ (b :: *)
    3. a ~ b
    4. (a :: *) ~ (b :: *)

2.

  1. a ~ b
  2. (a :: *) ~ (b :: *)
  3. a ~~ b
  4. (a :: *) ~~ (b :: *)

3.

  1. a ~~ c
  2. (a :: *) ~~ (c :: k)
  3. a ~~ c
  4. (a :: *) ~~ (c :: k)

4.

  1. a ~ b
  2. (a :: *) ~ (b :: *)
  3. a ~# b
  4. (a :: *) ~# (b :: *)

5.

  1. a ~~ c
  2. (a :: *) ~~ (c :: k)
  3. a ~# c
  4. (a :: *) ~# (c :: k)

6.

  1. Coercible a b
  2. Coercible * a b
  3. Coercible a b
  4. Coercible * a b

7.

  1. Coercible a b
  2. Coercible * a b
  3. a ~R# b
  4. (a :: *) ~R# (b :: *)

8.

  1. a ~R# c
  2. (a :: *) ~R# (c :: k)
  3. a ~R# c
  4. (a :: *) ~R# (c :: k)

Here are the rules:

  1. With -fprint-equality-relations, print the true equality relation.
  2. Without -fprint-equality-relations:
    1. If the equality is representational and homogeneous, use Coercible.
    2. Otherwise, if the equality is representational, use ~R#.
    3. If the equality is nominal and homogeneous, use ~.
    4. Otherwise, if the equality is nominal, use ~~.
  3. With -fprint-explicit-kinds, print kinds on both sides of an infix operator, as above; or print the kind with Coercible.
  4. Without -fprint-explicit-kinds, don't print kinds.

I believe that my examples above conform to these rules.

Do we agree with this approach?

comment:5 Changed 2 months ago by simonpj

That looks good to me.

comment:6 Changed 2 months ago by RyanGlScott

comment:4 sounds fine, but it only addresses problem (2). What about problem (1)? We still have GHC reporting that the kind of Coercible a b is TYPE (TupleRep '[]), which is utterly bogus.

It seems like if -fprint-equality-relations is disabled, then we'd want to print the kind Constraint instead, yes? Is that feasible with the way partial type signature reporting currently works?

Last edited 2 months ago by RyanGlScott (previous) (diff)

comment:7 Changed 2 months ago by goldfire

I think comment:6 is a red herring. Why is GHC attempting to report about ~R# at all here? The type of the hole is really Coercible a b. I don't think this is a pretty-printing issue.

Instead, the solver needs to be taught somewhere to transmute a ~R# b constraints to Coercible a b constraints. But where? Do we do this for nominal equality anywhere?

comment:8 Changed 2 months ago by simonpj

Instead, the solver needs to be taught somewhere to transmute a ~R# b constraints to Coercible a b constraints. But where? Do we do this for nominal equality anywhere?

We do not transmute unsolved a ~# b constraints into a ~ b. Rather we pretty-print the unsolved a ~# b constraint as a ~ b.

But if we do that and print the kind of the constraint, the two will be inconsistent. It appears that this only shows up for holes. Maybe we should refrain from printing the kind of a hole-filler if it's a constraint?

comment:9 Changed 5 weeks ago by RyanGlScott

Differential Rev(s): Phab:D4696
Status: newpatch

comment:10 Changed 5 weeks ago by Ben Gamari <ben@…>

In 99f8cc84/ghc:

Fix #15039 by pretty-printing equalities more systematically

GHC previously had a handful of special cases for
pretty-printing equalities in a more user-friendly manner, but they
were far from comprehensive (see #15039 for an example of where this
fell apart).

This patch makes the pretty-printing of equalities much more
systematic. I've adopted the approach laid out in
https://ghc.haskell.org/trac/ghc/ticket/15039#comment:4, and updated
`Note [Equality predicates in IfaceType]` accordingly. We are now
more careful to respect the properties of the
`-fprint-explicit-kinds` and `-fprint-equality-relations` flags,
which led to some improvements in error message outputs.

Along the way, I also tweaked the error-reporting machinery not to
print out the type of a typed hole when the type is an unlifted
equality, since it's kind (`TYPE ('TupleRep '[])`) was more
confusing than anything.

Test Plan: make test TEST="T15039a T15039b T15039c T15039d"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15039

Differential Revision: https://phabricator.haskell.org/D4696

comment:11 Changed 5 weeks ago by RyanGlScott

Cc: partial-sigs/should_compile/T15039a partial-sigs/should_compile/T15039b partial-sigs/should_compile/T15039c partial-sigs/should_compile/T15039d added
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.