"Type varible is ambiguous" - Why do the two codes behave differently?

Learn
1

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?

2

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 #-}
3

You need to turn on

{-# LANGUAGE ScopedTypeVariables #-}

to refer to n in the body of fromNat.

2 Likes
4

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.

5

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 ns 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
6

Thanks! Your explanation helps a lot!

1 Like
7

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