[Haskellcafe] Recursive constraints with type families
Dmitriy Matrosov
sgf.dma at gmail.com
Fri Jan 21 16:59:42 UTC 2022
Hi.
I've stumbled upon a simple problem with recursive type family:
> {# LANGUAGE RankNTypes #}
> {# LANGUAGE KindSignatures #}
> {# LANGUAGE TypeApplications #}
> {# LANGUAGE TypeOperators #}
> {# LANGUAGE PolyKinds #}
> {# LANGUAGE TypeFamilies #}
> {# LANGUAGE StandaloneKindSignatures #}
> {# LANGUAGE ScopedTypeVariables #}
> {# LANGUAGE UndecidableInstances #}
>
> import GHC.TypeLits
> import Data.Proxy
> import Data.Kind
>
> type C :: Nat > Constraint
> type family C x where
> C 0 = KnownNat 0
> C x = (KnownNat x, C (x  1))
> C x = (KnownNat x, C 0)
> C x = KnownNat x
>
> type C2 x = (KnownNat x, C2 1)
>
> showNat :: forall (n :: Nat). C n => Proxy n > String
> showNat _ = show $ natVal (Proxy @n)
and the error is
Prelude> :r
[1 of 1] Compiling Main ( constrainttypefamily.lhs, interpreted )
constrainttypefamily.lhs:31:22: error:
• Could not deduce (KnownNat n) arising from a use of ‘natVal’
from the context: C n
bound by the type signature for:
showNat :: forall (n :: Nat). C n => Proxy n > String
at constrainttypefamily.lhs:30:356
Possible fix:
add (KnownNat n) to the context of
the type signature for:
showNat :: forall (n :: Nat). C n => Proxy n > String
• In the second argument of ‘($)’, namely ‘natVal (Proxy @n)’
In the expression: show $ natVal (Proxy @n)
In an equation for ‘showNat’: showNat _ = show $ natVal (Proxy @n)

31  > showNat _ = show $ natVal (Proxy @n)
 ^^^^^^^^^^^^^^^^^
If i write just
C x = KnownNat x
everything works fine. I guess, the reason is UndecidableInstances, but why
and then, how can i build constraints recursively and make it work?
Thanks.
PS. Initially, this 'showNat' was something like
countDown :: forall (n :: Nat). C n => Proxy n > String
countDown _ = let x = natVal (Proxy @n)
in if x > 0
then show x ++ countDown (Proxy @(n  1))
else "end"
but it does not work.
More information about the HaskellCafe
mailing list