I’m learning type-level programming and written the following code:
import Data.Kind (Type)
data Nat = Z | S Nat
data SNat :: Nat -> Type where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
data Proxy :: Nat -> Type where
Proxy :: Proxy n
{- The following fails to compile
class FromNat (nat :: Nat) where
fromNat :: Proxy nat -> Nat
instance FromNat 'Z where
fromNat Proxy = Z
instance FromNat n => FromNat ('S n) where
fromNat Proxy = S $ fromNat (Proxy :: Proxy n)
--}
-- While the following compiles
class ToSNat (nat :: Nat) where
toSNat :: Proxy nat -> SNat nat
instance ToSNat 'Z where
toSNat Proxy = SZ
instance ToSNat n => ToSNat ('S n) where
toSNat Proxy = SS $ toSNat (Proxy :: Proxy n)
I think the two parts are rather similar but the first ends up in error:
• Could not deduce (FromNat nat0) arising from a use of ‘fromNat’
from the context: FromNat n
bound by the instance declaration at dtc.hs:29:10-36
The type variable ‘nat0’ is ambiguous
These potential instances exist:
instance FromNat n => FromNat ('S n) -- Defined at dtc.hs:29:10
instance FromNat 'Z -- Defined at dtc.hs:27:10
• In the second argument of ‘($)’, namely
‘fromNat (Proxy :: Proxy n)’
In the expression: S $ fromNat (Proxy :: Proxy n)
In an equation for ‘fromNat’:
fromNat Proxy = S $ fromNat (Proxy :: Proxy n)
So why it happens?