Injective type families
Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
I've naively attempted a proofofconcept in GHC. It's almost certainly incorrect and probably breaks the type system, but I thought it best to put it here and see if it can be made workable.
In summary, my changes are:

Add a new keyword,
injective
, which is available only when theTypeFamilies
extension is enabled. Injective families may then be defined thus:` injective family F a :: * type instance F Int = Bool type instance F Bool = Int
injective family G a :: * type instance G a = a `
Syntax is of course completely changeable; I've simply picked one of the possible designs. Hopefully this won't be subjected to too much bikeshedding.

Add the constructor
InjFamilyTyCon
toTyConRhs
and the family flavourInjectiveFamily
toHsSyn
. Again, I've opted to encode injectivity as a flavour rather than (say) aBool
attached to type families. This is a completely arbitrary choice and may be utterly stupid. 
Altered the definition of decomposable
TyCon
s to include injective families (isDecomposableTyCon
). This effectively introduces a typing rule that says if we have(F a ~ F b)
then we can deduce(a ~ b)
(TcCanonical
). 
Modified the unifier so that it will attempt to replace saturated injective families with their lefthand sides where possible (
TcUnify
). This means that in a function such as:f :: F a > F a f = ...
The type of f False
is inferred as F Int
(i.e., a
is no longer ambiguous).
Some things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate f False
I get nothing (not even a Segmentation fault).
See what you think.
Trac metadata
Trac field  Value 

Version  7.4.1 
Type  FeatureRequest 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  simonpj@microsoft.com 
Operating system  
Architecture 