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

Roberto Zunino 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 mailing list