[Haskell-cafe] type-level integers using type families

[Roberto Zunino]

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>>>

that

  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.

Zun.