Re: [GHC] #15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature

19 Apr 2018

      #15039: Bizarre pretty-printing of inferred Coercible constraint in partial type
signature
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.1
  checker)                           |             Keywords:
      Resolution:                    |  PartialTypeSignatures, TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (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`.

 2. Homogeneous use of heterogeneous equality `a ~~ b`.

 3. Heterogeneous use of heterogeneous equality `a ~~ c`.

 4. Homogeneous use of unlifted equality `a ~# b`.

 5. Heterogeneous use of unlifted equality `a ~# c`.

 6. Homegeneous representational equality `Coercible a b`.

 7. Homogeneous use of representational unlifted equality `a ~#R b`.

 8. 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

 a. By default
 b. With `-fprint-explicit-kinds`
 c. With `-fprint-equality-relations`
 d. With `-fprint-explicit-kinds -fprint-equality-relations`.

 I propose:

 1.
   a. `a ~ b`
   b. `(a :: *) ~ (b :: *)`
   c. `a ~ b`
   d. `(a :: *) ~ (b :: *)`

 2.
   a. `a ~ b`
   b. `(a :: *) ~ (b :: *)`
   c. `a ~~ b`
   d. `(a :: *) ~~ (b :: *)`

 3.
   a. `a ~~ c`
   b. `(a :: *) ~~ (c :: k)`
   c. `a ~~ c`
   d. `(a :: *) ~~ (c :: k)`

 4.
   a. `a ~ b`
   b. `(a :: *) ~ (b :: *)`
   c. `a ~# b`
   d. `(a :: *) ~# (b :: *)`

 5.
   a. `a ~~ c`
   b. `(a :: *) ~~ (c :: k)`
   c. `a ~# c`
   d. `(a :: *) ~# (c :: k)`

 6.
   a. `Coercible a b`
   b. `Coercible * a b`
   c. `Coercible a b`
   d. `Coercible * a b`

 7.
   a. `Coercible a b`
   b. `Coercible * a b`
   c. `a ~R# b`
   d. `(a :: *) ~R# (b :: *)`

 8.
   a. `a ~R# c`
   b. `(a :: *) ~R# (c :: k)`
   c. `a ~R# c`
   d. `(a :: *) ~R# (c :: k)`

 Here are the rules:

 A. With `-fprint-equality-relations`, print the true equality relation.
 B. Without `-fprint-equality-relations`:
    i. If the equality is representational and homogeneous, use
 `Coercible`.
    ii. Otherwise, if the equality is representational, use `~R#`.
    iii. If the equality is nominal and homogeneous, use `~`.
    iv. Otherwise, if the equality is nominal, use `~~`.
 C. With `-fprint-explicit-kinds`, print kinds on both sides of an infix
 operator, as above; or print the kind with `Coercible`.
 D. Without `-fprint-explicit-kinds`, don't print kinds.

 I believe that my examples above conform to these rules.

 Do we agree with this approach?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler