Type class instance checking can't detect "piecewise instances"

1
votes

I have a family of data types indexed by type-level integers, and I define them as instances of some type class in a "piecewise" manner, which causes problems when trying to derive instances of another class. To illustrate, I have isolated the problem as follows. Consider this code:

{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances,
             FlexibleInstances  , UndecidableInstances #-}

data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

class Nat n where
  toInt :: n -> Int

instance Nat Zero where
  toInt _ = 0
instance Nat One where ------------------------- START MODIFY
  toInt _ = 1
instance (Nat n) => Nat (Succ (Succ n)) where
  toInt _ = 2 + toInt (undefined :: n) --------- END MODIFY

This is a slight modification of the type-level integers defined in "Fun with type functions" by Kiselyov, Jones and Shan. This compiles fine and toInt seems to work as expected. Right now Nat contains all integers Zero, One, Two and so on.

However GHC complains after I add the following lines and recompile:

class LikeInt n where
  likeInt :: n -> Int

instance (Nat n) => LikeInt (Succ n) where
  likeInt = toInt

Error: Could not deduce the (Nat (Succ n)) arising from a use of "toInt" from the context (Nat n).

My guess is that when GHC infers that toInt has an argument of type Succ n, but the only instances for Nat are for Zero, Succ Zero and (Nat n0) => Succ (Succ n0), and Succ n matches to none of those. This guess is supported by a successful compile when I replace the MODIFY block with the original

instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: n)

How can I get likeInt to work just like toInt, even with the modified block? This is important for my actual project.

2
haskellcompiler-errorstype-inferencetypeclasstype-families
I'd like to note here that with modern GHC features and libraries (closed type families, data kinds, singletons) we have more powerful and convenient type-level programming facilities than what's presented in the quoted paper. – András Kovács
Also, why can't you have the modified instances for Nat? – András Kovács
The modified instances compile, but when I try to derive instances for LikeInt it fails. – Herng Yi

2 Answers

0
votes

Can't you just define this instance?

instance Nat n => LikeInt n where
  likeInt = toInt

*Main> likeInt (undefined :: Zero)
0
*Main> likeInt (undefined :: One)
1
*Main> likeInt (undefined :: Two)
2
*Main> likeInt (undefined :: Three)
3

Or would you like to avoid the Nat constraint?

0
votes

The compiler told you what to do.

You had

instance (Nat n) => LikeInt (Succ n) where
  likeInt = toInt

And the compiler said:

Could not deduce (Nat (Succ n)) arising from a use of ‘toInt’
from the context (Nat n)

So we change the context to give the constraint the compiler asked for. Magic!

instance (Nat (Succ n)) => LikeInt (Succ n) where
  likeInt = toInt

(and this indeed compiles).