Roberto Zunino wrote:
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.
Yes, that's exactly what I want, but for type families (not MPTC). I think it could be done if the type arguments were matched one at a time, across all visible instances. So given
data True data False
type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z
the first argument (x) of Cond would be matched before y and z are inferred. Then if x is True, the type checker would see that z is never used on the RHS, so it would not bother trying to infer it at all.
If we had subtyping, typing that as Top would suffice, I believe.
Zun.