CODEWITHSUNDEEP
haskellrecursiontypeclass
nicolas
nicolas

Reputation: 9835

recursive instances in haskell

When using the following code, I get the error message below for the recursive usage of toInt 

module Intro0 where
data Zero
data Succ n

class Nat n where
  toInt :: n -> Int
instance Nat Zero where
  toInt _ = 0
instance (Nat n) => Nat (Succ n) where
  toInt _ = (1::Int) + toInt (undefined :: n)

I would have imagined finding toInt is trivial as it is specified in the context of the recursive instance, but I get a unification problem

Could not deduce (Nat n0) arising from a use of ‘toInt’
    from the context (Nat n)
      bound by the instance declaration
      at EPhantomTypes.hs:10:10-32
    The type variable ‘n0’ is ambiguous
    Note: there are several potential instances:
      instance Nat n => Nat (Succ n)
        -- Defined at EPhantomTypes.hs:10:10
      instance Nat Zero
        -- Defined at EPhantomTypes.hs:8:10
    In the second argument of ‘(+)’, namely ‘toInt (undefined :: n)’
    In the expression: (1 :: Int) + toInt (undefined :: n)
    In an equation for ‘toInt’:
        toInt _ = (1 :: Int) + toInt (undefined :: n)

I am not sure why this is. It looks trivial but I am not sure what to do with this.

Obviously n and n0 should be the same but even using 

instance forall n . (Nat n) => Nat (Succ n) where

leads to the same error message

Upvotes: 2

Views: 394

Answers (1)

Alec
Alec

Reputation: 32329

The problem pertains to the scope of the variable n. In particular, the n in (undefined :: n) isn't the same n as in (Nat n) => Nat (Succ n). If you would like to change this, you can enable -XScopedTypeVariables (or add {-# LANGUAGE ScopedTypeVariables #-} to the top of your file), and then the two ns will be the same and everything compiles.

Upvotes: 7

Related Questions