Hi Olaf,
Then the compiler rightfully complains that someone could write an instance Index (a,b) n
Do you expect that to happen in practice or is that only a theoretical possibility? (If you could tell GHC that "Index (a, b) n" is forever forbidden, would you?) Have you considered using a constructor to disambiguate pairs (a, b) from singletons: newtype Singleton a = Sg a instance Index a n => Range (Singleton a) n n or using overlapping instances and an explicit equality constraint to ensure that the pair instance is a "substitution instance" of the singleton instance: instance {-# OVERLAPPABLE #-} (Index a n, n ~ n') => Range a n n' or a hybrid approach with both Singleton (instead of overlap) and the explicit equality constraint (for more general type inference): instance (Index a n, n ~ n') => Range (Singleton a) n n' Cheers, Li-yao On 9/16/19 3:08 PM, Olaf Klinke wrote:
Dear Cafe,
I had a lengthy discussion with GHC but so far it won't let me do the following. (Code below is simplified to transport the idea. Type families don't seem to do the trick, either.) A finite set of types A, B, C, ... is totally ordered. This can be expressed e.g. by a multi-parameter type class and type-level natural numbers:
instance Index A 0 where instance Index B 1 where etc.
Now I want a type class Range and an appropriate set of instance declarations that has A, B, (A,B), (A,C), (A,(B,C)) etc. as members but not (B,A) or (C,C). That is, each type appears at most once and in the defined order.
The problem is overlapping instances of the base case with the inductive case.
instance Index a n => Range a n n instance (Range a x y, Range b x' y', y < x') => Range (a,b) x y'
Then the compiler rightfully complains that someone could write an instance Index (a,b) n which would lead to conflicting instances of Range (a,b) n n. I can not make either of the type classes Index nor Range closed because there will be several of those sets of types. This problem is like smart constructors for ordered lists, but on the type level.
Thanks in advance for any hints. Olaf
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.