[GHC] #16146: Trivial partial type signature kills type inference in the presence of GADTs

[GHC]

#16146: Trivial partial type signature kills type inference in the presence of
GADTs
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Why does quantification enter into it, now that I think of it?

 Let's look at some typing rules, where `<=` denotes checking and `=>`
 denotes inference in the bidirectional type system. I use `t` to denote a
 type (no wildcards) and `p` to denote a partial type (zero or more
 wildcards).

 {{{
 e <= t
 ------------ Sig
 (e : t) => t

 e => t1
 t1 <: t2
 -------- Infer
 e <= t2
 }}}

 These rules govern what happens when an expression with a complete type
 signature `(e : t1)` is checked against a type `t2`. Because there is no
 `<=` rule for the `(e : t1)` form, we use the Infer rule to switch into
 synthesis mode. Since we have `t1` as the type signature, we synthesize
 type `t1` for `(e : t1)`. Then, we check to make sure that `t1` is a
 subtype of `t2`. (Reminder: `t1` is a subtype of `t2` iff there is a
 computationally free way to convert a value of type `t1` to a value of
 type `t2`. Example: `forall a. a -> a` is a subtype of `Int -> Int`
 because we can instantiate a value of type `forall a. a -> a` with `Int`
 with no runtime cost.)

 Currently, this is the rule for an expression with a partial type
 signature:

 {{{
 e <~~ p => t
 ------------ PartialSig
 (e : p) => t
 }}}

 where `e <~~ p => t` means that checking `e` against partial signature `p`
 results in a type `t`. This is done by GHC's `simplifyInfer`.

 I propose adding a new rule to the system:

 {{{
 p <: t2 => p2
 e <~~ p2 => t
 t <: t2
 ------------- PartialSigCheck
 (e : p) <= t2
 }}}

 where `p <: t2 => p2` means:
 1. Check whether `p` is a subtype of `t2`.
 2. During this check, we might have to choose values for wildcards in `p`.
 3. `p2` is `p`, but with the wildcards zonked to have the values
 discovered in the subtype check.

 Note that `p2` might actually have no wildcards left. Regardless, we will
 use the `e <~~ p2 => t` (`simplifyInfer`) operation, as checking against a
 partial type signature is really quite different than checking against a
 complete type signature, and we wouldn't want unifications with the
 pushed-down type to chane this. Naturally, we have to do another subtype
 check, just to make sure that the type after `simplifyInfer` is suitable.
 (It's possible that we can prove that if `p <: t2 => p2` and `e <~~ p2 =>
 t`, then `t <: t2`. Indeed, that would be desirable. But I'm not sure
 right now if this would be true.)

 I ''think'' that would solve our problem. And it seems to make GHC
 strictly more expressive. And it would seem to be "what the user would
 expect", making use of information manifestly available (but, today,
 ignored).

 This would require writing a new subtyping check `p <: t2 => p2`. The
 implementation of subtyping in GHC is somewhat laborious, but it's not a
 particularly complicated judgment. It's unclear how much code-sharing this
 new form would have with the existing one, given the different way that
 partial types are represented internally.

 I agree that this is a GHC proposal. However, the consequences of this are
 subtle and hard to predict, so I want to have some debate here before
 going there.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16146#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler