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?
Besides, I’m using these extensions:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-missing-export-lists #-}
You need to turn on
{-# LANGUAGE ScopedTypeVariables #-}
to refer to n
in the body of fromNat
.
2 Likes
Thank you a lot! Turning on the extension does work. But I still wonder what is the difference between the two parts. I mean, why toSNat
can compile even without the extension.
The type of toSNat
is Proxy nat -> SNat nat
, which in the recursive instance is Proxy ('S n) -> SNat ('S n)
. So the expression SS $ toSNat (Proxy :: Proxy n)
is being checked against the type SNat ('S n)
. GHC doesn’t initially know that the two n
s are the same, but that doesn’t matter because checking the expression unifies them. You could omit the :: Proxy n
from that instance and it would still work.
In contrast, the type of fromNat
is Proxy nat -> Nat
, and the RHS of the recursive instance is being checked against Nat
. Now GHC is adrift, because there’s nothing for the n
to unify with. Enabling ScopedTypeVariables
tells GHC that the n
is the specific n
from the instance signature and not some unknown type, which in this case is necessary because GHC can’t figure it out from the member signature.
3 Likes
Thanks! Your explanation helps a lot!
1 Like
Yes, or to put it another way, you don’t need the type signature at all in toSNat
:
instance ToSNat n => ToSNat ('S n) where
toSNat Proxy = SS $ toSNat Proxy
EDIT: Oh, I see @rhendric actually already said that, and I skimmed too fast.
1 Like