I have a typeclass, which imposes a
class KnownNat (Card a)=> HasFin a wheretype Card a :: Nat...
And, I have instances of this class for several basic "building block" types:
instance HasFin () wheretype Card ()=1...instance HasFin Bool wheretype Card Bool=2...
I plan to build many "composite" types out of these building block types, using sums and products. Currently, I'm having to explicitly write a composite
KnownNat constraint, when I instance
HasFin for one of these composite types:
instance (HasFin a, HasFin b, KnownNat (Card a + Card b))=> HasFin (Either a b) wheretype Card (Either a b)=Card a + Card b...
I would really like to not have to write:
KnownNat (Card a + Card b), in the code above.
Is there any type checker plug-in, which is capable of automatically extrapolating from
(HasFin a, HasFin b)=> to
(KnownNat (Card a + Card b))=> ?
Failing that, can I write an entailment, which provides the same extrapolation?