[GHC] #12680: Permit type equality instances in signatures

[GHC]

#12680: Permit type equality instances in signatures
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  backpack
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 ezyang):

 One way to help disentangle the difference between generativity and
 nominal distinctness is to look at the meaning of abstract types in
 signatures in an elaboration to a simpler language like Haskell!

 When I write a unit:

 {{{
 unit p where
   signature A where
     data T
     data S
   module M where
     import A
     f :: T ~ S => a -> b
     f x = x
 }}}

 I am effectively defining a Haskell program along the lines (with a little
 cheating to have structural records):

 {{{
 p :: forall t s. { f :: forall a b. t ~ s => a -> b }
 p = { f = \x -> x } -- ill-typed
 }}}

 When I am typechecking the body of p, `t ~ s` clearly does not hold, as
 `t` and `s` are both skolem variables and aren't available for
 unification. But that doesn't mean that we can treat the body of `f` as
 inaccessible: obviously if I invoke p as `p @Int @Int`, `Int ~ Int` is
 provable.

 What Backpack takes advantage of is the outrageous coincidence between
 skolem variables and abstract types. This should not at all be surprising,
 since abstract types are existential types, and (∃x. τ) -> τ' is
 equivalent to ∀x. (τ -> τ'). We want to treat abstract types like skolem
 variables, and I conjecture that the rules for OutsideIn(X) are compatible
 with this treatment, except for a few simplification rules (like eager
 failure when a given does not canonicalize). This would be good to pose
 formally and check with the paper.

 I think this also explains the confusing tension between "abstract data is
 generative" but "type synonyms are not generative, and thus should not be
 allowed to implement abstract data". Skolem variables are extremely well
 behaved: they can only be instantiated by types, so if we have `s :: * ->
 *` no one is going to set `s ~ S`, where `type S a = ...`. `S` is just not
 a valid type. And of course, all types are "generative" in the sense
 described earlier. (Instances (and the need for abstract types to be
 implemented without type families) are a giant fly in the ointment, but we
 are punting on soundness in this case *anyway*, so I am not inclined to
 look to closely at the matter.)

 The claim that T does not unify with S, EVER (as is the case in an hs-boot
 file) is a very unnatural claim that would be difficult to translate into
 Haskell via this elaboration. I would argue this is more of an artifact of
 how we have implemented hs-boot files over anything else (if we had
 shaping, this "nominal distinctness" wouldn't even hold there.)

 tl;dr: Abstract types in signatures are skolem variables spelled with
 capital letters; the rules for inference with abstract types are the same
 as the rules for inference with skolem variables (modulo early failure
 when givens fail to canonicalize). You can instantiate skolem variables
 with whatever you want.

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