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/