[Haskell-cafe] type-level integers using type families
zunino at di.unipi.it
Fri May 30 08:14:40 EDT 2008
Manuel M T Chakravarty wrote:
> Peter Gavin:
>> will work if the non-taken branch can't be unified with anything. Is
>> this planned? Is it even feasible?
> I don't think i entirely understand the question.
Maybe he wants, given
cond :: Cond x y z => x -> y -> z
tt :: True
true_exp :: a
false_exp :: <<<untypable>>>
cond tt true_exp false_exp :: a
That is the type of false_exp is "lazily inferred", so that type errors
do not make inference fail if they show up in an unneeded place.
If we had subtyping, typing that as Top would suffice, I believe.
More information about the Haskell-Cafe