Re: [Haskell-cafe] Recursive constraints with type families

21 Jan 2022

      Hi!

In order for you to reach any of the cases in C, the type family must be
able to see if x is 0 or not. However, you're passing it an arbitrary n, so
it has no way of knowing which case it should pick.

GHC doesn't do any reasoning of the sort "well this constraint is
available in all the cases of the type family, so I'll just add it".

The solution here would be to separate your KnownNat constraint from
whatever you want to calculate in your recursive type family:

type C1 n = (KnownNat n, C n)
type family C n ...

countDown :: forall (n :: Nat). C1 n => Proxy n -> String
countDown = ...

Cheers,

Georgi

On Fri, Jan 21, 2022 at 7:00 PM Dmitriy Matrosov  wrote:
...
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 mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

Re: [Haskell-cafe] Recursive constraints with type families

Georgi Lyubenov