#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): OK, after a bit of hacking, I have a much better, gloriously simple solution: 1. `data T` in hs-boot is treated as a "nominally distinct abstract type", whereas `data T` in hsig is treated as "totally abstract type"; the difference being that T may become definitionally equal to another type at some later point. 2. When unifying TyCons in the type inference, when we would hard failure because a totally abstract TyCon doesn't unify with something else, we *instead* treat the constraint as irreducible and continue on. This prevents `f :: (H1.T ~ H2.T) => a -> b` from being treated as inaccessible. There may be some other cases I need to handle, but this is the big one. 3. We continue to assume that abstract data is injective; e.g., `(T a ~ T b) => a -> b` should hold when T is totally abstract. When accepting a type synonym implementation of data, we need to ensure that it is injective. This can be done easily by (1) excluding any type synonyms which contain type families, and (2) ensuring that all type parameters of the type synonym are used (since "phantom" type parameters are not injective). 4. If someone DOESN'T want us to assume that `T` is injective, they should declare an open type family instead ala `type family T a` instead of `data T a`. I suppose we should permit such a declaration to be *implemented* using a type synonym, but this doesn't seem very urgent since you can always write `type instance T a = Blah a` instead. No more nonsense with open type families. Phabricator incoming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12680#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler