[Haskell-cafe] Recursive constraints with type families

[Li-yao Xia]

On 2022-01-26 9:51 AM, Dmitriy Matrosov wrote:
> So, the key of this trick is to make impossible to unfold type family 
> without
> evaluating 'If' ?
>

Yes!

> I need something like
> 
>      type instance F.Eval (C2' 0) = (() :: Constraint)
>      type instance F.Eval (C2' x) = (KnownNat x, F.Eval (C2' (x - 1)))
> 
> which does not compile. Thus, i need If to be an argument for Eval (like in
> your code below), so ghc is forced to evaluate it to unfold type family
> further. Does this sound correct?

That sounds correct.

Another problem with closed type families here is that there is no 
construct for "x is not 0" that would let you know to take the branch "C 
x = (KnownNat x, C (x-1))". The general workaround used here is to turn 
the comparison to a boolean and then reify that boolean. At that point, 
you don't have to use `If`, you can also declare a new type family to 
match on that boolean, but it gets tedious for the same reason we use 
"if" at the term level rather than defining a new function for every 
conditional.

> So, i can't use plain Bool with something like
> 
>      class IsBool b where
>          getBool :: Proxy b -> Bool
> 
> because in that case both True and False branches of case would have the 
> same
> type and ghc can't figure out by looking at plain Bool whether type level
> condition (n F.> 0) was true or false, right?
> 

Indeed.

> So, does ghc take condition from getBool application 
> literally
> and then uses its result to evaluates If in type family?

That's right, GHC just takes the condition literally, it has no 
understanding of the meaning of `>` and `+` to draw logical inferences 
about them.

Nevertheless, you might be interested in ghc-typelits-natnormalize, a 
plugin which equips GHC with a few such reasoning capabilities. Or 
Liquid Haskell, for an even more powerful approach.

https://hackage.haskell.org/package/ghc-typelits-natnormalise
https://ucsd-progsys.github.io/liquidhaskell/