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

[Peter Gavin]

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