[Haskell-cafe] Recursive constraints with type families

[Georgi Lyubenov]

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 <sgf.dma at gmail.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220121/477c32f5/attachment.html>