[Haskell-cafe] Recursive constraints with type families

21 Jan 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             ( 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.

[Haskell-cafe] Recursive constraints with type families

Dmitriy Matrosov