[Haskell-cafe] Recursive constraints with type families

[Dmitriy Matrosov]

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             ( constraint-type-family.lhs, interpreted )

     constraint-type-family.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 constraint-type-family.lhs:30:3-56
           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.