<div dir="ltr">Hi!<br><br>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.<br><br>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".<br><br>The solution here would be to separate your KnownNat constraint from whatever you want to calculate in your recursive type family:<br><br>type C1 n = (KnownNat n, C n)<br>type family C n ...<br><br>countDown :: forall (n :: Nat). C1 n => Proxy n -> String<br>countDown = ...<br><br>Cheers,<br><br>Georgi</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 21, 2022 at 7:00 PM Dmitriy Matrosov <<a href="mailto:sgf.dma@gmail.com">sgf.dma@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi.<br>
<br>
I've stumbled upon a simple problem with recursive type family:<br>
<br>
> {-# LANGUAGE RankNTypes #-}<br>
> {-# LANGUAGE KindSignatures #-}<br>
> {-# LANGUAGE TypeApplications #-}<br>
> {-# LANGUAGE TypeOperators #-}<br>
> {-# LANGUAGE PolyKinds #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> {-# LANGUAGE StandaloneKindSignatures #-}<br>
> {-# LANGUAGE ScopedTypeVariables #-}<br>
> {-# LANGUAGE UndecidableInstances #-}<br>
><br>
> import GHC.TypeLits<br>
> import Data.Proxy<br>
> import Data.Kind<br>
><br>
> type C :: Nat -> Constraint<br>
> type family C x where<br>
>     C 0 = KnownNat 0<br>
>     --C x = (KnownNat x, C (x - 1))<br>
>     C x = (KnownNat x, C 0)<br>
>     --C x = KnownNat x<br>
><br>
> --type C2 x = (KnownNat x, C2 1)<br>
><br>
> showNat :: forall (n :: Nat). C n => Proxy n -> String<br>
> showNat _ = show $ natVal (Proxy @n)<br>
<br>
and the error is<br>
<br>
     Prelude> :r<br>
     [1 of 1] Compiling Main             ( constraint-type-family.lhs, interpreted )<br>
<br>
     constraint-type-family.lhs:31:22: error:<br>
         • Could not deduce (KnownNat n) arising from a use of ‘natVal’<br>
           from the context: C n<br>
             bound by the type signature for:<br>
                        showNat :: forall (n :: Nat). C n => Proxy n -> String<br>
             at constraint-type-family.lhs:30:3-56<br>
           Possible fix:<br>
             add (KnownNat n) to the context of<br>
               the type signature for:<br>
                 showNat :: forall (n :: Nat). C n => Proxy n -> String<br>
         • In the second argument of ‘($)’, namely ‘natVal (Proxy @n)’<br>
           In the expression: show $ natVal (Proxy @n)<br>
           In an equation for ‘showNat’: showNat _ = show $ natVal (Proxy @n)<br>
        |<br>
     31 | > showNat _ = show $ natVal (Proxy @n)<br>
        |                      ^^^^^^^^^^^^^^^^^<br>
<br>
If i write just<br>
<br>
      C x = KnownNat x<br>
<br>
everything works fine. I guess, the reason is UndecidableInstances, but why<br>
and then, how can i build constraints recursively and make it work?<br>
<br>
Thanks.<br>
<br>
PS. Initially, this 'showNat' was something like<br>
<br>
     countDown :: forall (n :: Nat). C n => Proxy n -> String<br>
     countDown _ = let x = natVal (Proxy @n)<br>
                   in  if x > 0<br>
                         then show x ++ countDown (Proxy @(n - 1))<br>
                         else "end"<br>
<br>
but it does not work.<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>