#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):
If T and S are datatypes, then how could they be equal?
``data S`` can be implemented with ``type S = T``, thus making them equal. Admittedly the use of ``data X`` to represent an abstract data type is awful, arguably we should get the syntax ``type X`` working which is a bit clearer.
And your `F Int ~ S` seems like it could just be an instance of the type family.
Yes, I think you're right. The important thing is that if you write a type family instance in a signature, it does not indicate that there is *exactly* this reduction rule in the type family, just that it is derivable (though, what about injective type families? Ick.) David was specifically interested in playing around with alternative axiomatizations of type families by specifying equalities manually. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12680#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler