#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