[Haskell-cafe] Strange problem with type classes (ghc 6.8.2 looks allright and ghc 6.10.1 doesn't).

22 Sep 2009

      I try to create yet another hardware description language embedded in
Haskell and faced a (perceived) bug in ghc 6.10.1 type checker. In ghc
6.8.2 everything works fine.

I need a type class that can express relationship between type and
its' "size in wires" (the number of bits needed to represent any value
of a type). The type class can be easily generalized to most haskell
data types and it's easy to write instance derivation using Template
Haskell.

I used multiparameter type classes because support for type families
in Template Haskell was incomplete in 6.10.1 and prior versions.

The source code below.

Do not forget to include -fcontext-stack=100 when trying to load the
code into ghci. The problem lines are between "THE PROBLEM!!"
comments.

Please, tell me, is it geniune bug or I misunderstand something about
Haskell type checker? How do you solve problems like that?

and, btw, you can take a look on how we can describe something
MIPS-alike in Haskell here: http://thesz.mskhug.ru/svn/hhdl/MIPS.hs

it is not finished by any means, but it gives a feel on how it will
look. I head to obtain (pretty) efficient simulation functions on
infinite streams (almost done, transformations are very simple) and
synthesable VHDL/Verilog description all from the same code that looks
like ordinary Haskell code.
-----------------------------------------------------------------------------------------------------------------------------
-- "A problem with functional dependencies.
-- use -fcontext-stack=100 ghc switch.

{-# LANGUAGE GADTs, FunctionalDependencies, MultiParamTypeClasses,
TypeSynonymInstances, FlexibleInstances, FlexibleContexts,
UndecidableInstances #-}

module Problem where

import Data.Bits
import Data.Word

-------------------------------------------------------------------------------
-- Type level arithmetic.

data Zero = Zero
data Succ n = Succ n

type ZERO = Zero
type ONE = Succ ZERO
type TWO = Succ ONE
type THREE = Succ TWO
type FOUR = Succ THREE
type FIVE = Succ FOUR
type SIX = Succ FIVE
type SEVEN = Succ SIX
type EIGHT = Succ SEVEN
type NINE = Succ EIGHT
type SIZE10 = Succ NINE
type SIZE11 = Succ SIZE10
type SIZE12 = Succ SIZE11
type SIZE13 = Succ SIZE12
type SIZE15 = Succ (Succ SIZE13)
type SIZE16 = Succ SIZE15
type SIZE20 = Succ (Succ (Succ (Succ (Succ SIZE15))))
type SIZE25 = Succ (Succ (Succ (Succ (Succ SIZE20))))
type SIZE26 = Succ SIZE25
type SIZE30 = Succ (Succ (Succ (Succ (Succ SIZE25))))
type SIZE32 = Succ (Succ SIZE30)

class Nat n where fromNat :: n -> Int

instance Nat Zero where fromNat = const 0
instance Nat n => Nat (Succ n) where fromNat ~(Succ n) = 1+fromNat n

class (Nat a, Nat b, Nat c) => CPlus a b c | a b -> c, a c -> b

--instance Nat a => CPlus a Zero a
instance Nat a => CPlus Zero a a
instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus a (Succ b) (Succ c)

class (Nat a, Nat b, Nat c) => CMax a b c | a b -> c
instance CMax Zero Zero Zero
instance Nat a => CMax (Succ a) Zero (Succ a)
instance Nat a => CMax Zero (Succ a) (Succ a)
instance CMax a b c => CMax (Succ a) (Succ b) (Succ c)

class (Nat a, Nat b) => CDbl a b | a -> b
instance CPlus a a b => CDbl a b

class (Nat a, Nat b) => CPow2 a b | a -> b
instance CPow2 Zero (Succ Zero)
instance (CPow2 a b, CDbl b b2) => CPow2 (Succ a) b2

-------------------------------------------------------------------------------
-- Sized integer.

data IntSz n where
	IntSz :: Nat sz => Integer -> IntSz sz

intSzSizeType :: IntSz n -> n; intSzSizeType _ = undefined
intSzSize :: Nat n => IntSz n -> Int; intSzSize n = fromNat $ intSzSizeType n

instance Nat sz => Eq (IntSz sz) where
	(IntSz a) == (IntSz b) = a == b

instance Show (IntSz n) where
	show n@(IntSz x) = show x++"{"++show (intSzSize n)++"}"

instance Nat sz => Num (IntSz sz) where
	fromInteger x = IntSz x
	(IntSz a) + (IntSz b) = IntSz $ a+b
	(IntSz a) - (IntSz b) = IntSz $ a-b
	(IntSz a) * (IntSz b) = IntSz $ a*b
	abs = error "No abs for IntSz."
	signum = error "No signum for IntSz."

-------------------------------------------------------------------------------
-- ToWires class, the main source of problems.

class Nat aSz => ToWires a aSz | a -> aSz where
	wireSizeType :: a -> aSz
	wireSizeType _ = undefined
	-- size of a bus to hold a value in bits.
	wireSize :: a -> Int
	wireSize x = fromNat $ wireSizeType x
	-- 2^wireSize, currently unused.
	wireMul :: a -> Integer
	wireMul x = Data.Bits.shiftL 1 (wireSize x)
	-- selector size for decode (unused).
	wireSelSize :: a -> Int
	wireSelSize = const 0
	-- Integer should occupy no more than wireSize bits, the remaining
bits should be 0
	toWires :: a -> Integer
	-- fromWires should work with integers that have non-zero bits
	-- above wireSize index.
	fromWires :: Integer -> a
	-- enumeration.
	-- valuesCount of (Maybe a) returns 1+valuesCount (x::a)
	-- valuesCount of Either a b returns valuesCount (x::a) + valuesCount (yLLb)
	-- valuesCount of (a,b) returns valuesCoutn (x::a) * valuesCount (y::b)
	valuesCount :: a -> Integer
	-- valueIndex.
	-- get a value and return an index inside enumeration.
	valueIndex :: a -> Integer

-------------------------------------------------------------------------------
-- Instances.

instance (ToWires x a,ToWires y b, CPlus a b c) => ToWires (x,y) c where
	toWires (a,b) = Data.Bits.shiftL (toWires a) (wireSize b) .|. toWires b
	fromWires x = (a,b)
		where
			b = fromWires x
			a = fromWires $ Data.Bits.shiftR x (wireSize b)
	valuesCount (a,b) = valuesCount a*valuesCount b
	valueIndex (a,b) = valueIndex a*valuesCount b + valueIndex b

instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,
	CPlus b c bc, CPlus a bc abc) =>
	ToWires (x1,x2,x3) abc where
	toWires (a,b,c) = toWires (a,(b,c))
	fromWires abc = (a,b,c)
		where
			(a,(b,c)) = fromWires abc
	valuesCount (a,b,c) = valuesCount (a,(b,c))
	valueIndex (a,b,c) = valueIndex (a,(b,c))

instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,ToWires x4 d,ToWires x5 e,
	CPlus d e de, CPlus c de cde, CPlus b cde bcde, CPlus a bcde abcde) =>
	ToWires (x1,x2,x3,x4,x5) abcde where
	toWires (a,b,c,d,e) = toWires (a,(b,(c,(d,e))))
	fromWires abcde = (a,b,c,d,e)
		where
			(a,(b,(c,(d,e)))) = fromWires abcde
	valuesCount (a,b,c,d,e) = valuesCount (a,(b,(c,(d,e))))
	valueIndex (a,b,c,d,e) = valueIndex (a,(b,(c,(d,e))))

instance CPow2 FIVE size32 => ToWires Int size32 where
	toWires n = fromIntegral n .&. 0xffffffff
	fromWires x = fromIntegral x
	valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
	valueIndex = fromIntegral

instance CPow2 FIVE size32 => ToWires Word32 size32 where
	toWires n = fromIntegral n .&. 0xffffffff
	fromWires x = fromIntegral x
	valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
	valueIndex = fromIntegral

instance Nat size => ToWires (IntSz size) size where
	toWires x@(IntSz n) = n .&. (Data.Bits.shiftL 1 (wireSize x) - 1)
	fromWires x = fromIntegral x
	valuesCount x = Data.Bits.shiftL (1::Integer) (wireSize x)
	valueIndex x = toWires x

-------------------------------------------------------------------------------
-- Neccessary types for a problem.

-- A hack around bugs (??) in ghc 6.10.1.
data RI = RI (IntSz FIVE)
	deriving (Eq,Show)
data Imm5 = Imm5 (IntSz FIVE)
	deriving (Eq,Show)
data Imm16 = Imm16 (IntSz SIZE16)
	deriving (Eq,Show)
data Imm26 = Imm26 (IntSz SIZE26)
	deriving (Eq,Show)

instance ToWires RI FIVE where
	toWires (RI x) = toWires x
	fromWires x = RI $ fromWires x
	valuesCount = const 32
	valueIndex (RI x) = toWires x

instance ToWires Imm5 FIVE where
	toWires (Imm5 x) = toWires x
	fromWires x = Imm5 $ fromWires x
	valuesCount = const 32
	valueIndex (Imm5 x) = toWires x

instance ToWires Imm16 SIZE16 where
	toWires (Imm16 x) = toWires x
	fromWires x = Imm16 $ fromWires x
	valuesCount (Imm16 x) = valuesCount x
	valueIndex (Imm16 x) = valueIndex x

instance ToWires Imm26 SIZE26 where
	toWires (Imm26 x) = toWires x
	fromWires x = Imm26 $ fromWires x
	valuesCount (Imm26 x) = valuesCount x
	valueIndex (Imm26 x) = toWires x

instance ToWires a sz => ToWires (Maybe a) (Succ sz) where
	toWires Nothing = 0
	toWires (Just x) = shiftL (toWires x) 1 .|. 1
	fromWires = undefined
	valuesCount x = 1+valuesCount y
		where
			~(Just y) = x

	valueIndex Nothing = 0
	valueIndex (Just x) = 1+valueIndex x

-------------------------------------------------------------------------------
-- And a problem itself.

data Signed = Signed | Unsigned
	deriving (Eq,Show)

data MIPSCmd regv =
		Nop
	|	Trap
	-- we mark destination register with RI. It never gets fetched.
	-- we mark source registers as regv, because they can change their size
	-- at FETCH stage (became Word32).
	|	AddU	regv regv RI
	|	And	regv regv RI
	|	Div	Signed regv regv
	deriving (Eq,Show)

instance ToWires Signed (Succ Zero) where
	toWires (Signed) = Data.Bits.shiftL 0 1 .|. 0
	toWires (Unsigned) = Data.Bits.shiftL 0 1 .|. 1
	fromWires x = undefined
	valuesCount x = 1 + (1 + 0)
		where
			~(Signed) = x
			~(Unsigned) = x
	valueIndex x = case x of
		Signed -> 0 + 0
		Unsigned -> (0 + 0) + 0
		where
			~(Signed) = x
			~(Unsigned) = x

instance (ToWires regv_0 v_1, ToWires RI v_2,
	CPlus v_1 v_1 vCPlus_3, CPlus vCPlus_3 v_2 vCPlus_4,
	CPlus v_1 v_1 vCPlus_5, CPlus vCPlus_5 v_2 vCPlus_6,
	ToWires Signed v_7, CPlus v_7 v_1 vCPlus_8, CPlus vCPlus_8 v_1 vCPlus_9,
	CMax vCPlus_4 vCPlus_6 vCMax_10, CMax vCMax_10 vCPlus_9 vCMax_11)
	=> ToWires (MIPSCmd regv_0) (Succ (Succ (Succ vCMax_11))) where

	toWires (Nop) = Data.Bits.shiftL 0 3 .|. 0
	toWires (Trap) = Data.Bits.shiftL 0 3 .|. 1
	toWires (AddU a_12 a_13 a_14) =
		Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_12) .|. toWires a_12) (wireSize a_13)
.|. toWires a_13) (wireSize a_14) .|. toWires a_14) 3 .|. 2
	toWires (And a_15 a_16 a_17) =
		Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_15) .|. toWires a_15) (wireSize a_16)
.|. toWires a_16) (wireSize a_17) .|. toWires a_17) 3 .|. 3
	toWires (Div a_18 a_19 a_20) =
		Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_18) .|. toWires a_18) (wireSize a_19)
.|. toWires a_19) (wireSize a_20) .|. toWires a_20) 3 .|. 4
	fromWires x = undefined
	valuesCount x = 1 + (1 + ((valuesCount x_21 * (valuesCount x_22 *
(valuesCount x_23 * 1))) + ((valuesCount x_24 * (valuesCount x_25 *
(valuesCount x_26 * 1))) + ((valuesCount x_27 * (valuesCount x_28 *
(valuesCount x_29 * 1))) + 0))))
		where
			~(Nop) = x
			~(Trap) = x
			~(AddU x_21 x_22 x_23) = x
			~(And x_24 x_25 x_26) = x
			~(Div x_27 x_28 x_29) = x
	-- Please don't mind that code is wrong, I can't get past typechecker here.
	valueIndex x = case x of
		Nop -> 0 + 0
		Trap -> (0 + 0) + 0
-- THE PROBLEM!!!
		AddU ax_30 ax_31 ax_32 ->
			((0 + 0) + 0) + valueIndex (ax_32,(ax_30, ax_31))
-- /THE PROBLEM!!!
{-
                                 And x_33 x_34 x_35 -> (((0 + 0) + 0)
+ valuesCount (x_32,

              (x_30,

               x_31))) + valueIndex (x_35,

                                     (x_33,

                                      x_34))
                                 Div x_36 x_37 x_38 -> ((((0 + 0) + 0)
+ valuesCount (x_32,

               (x_30,

                x_31))) + valuesCount (x_35,

                                       (x_33,

                                        x_34))) + valueIndex (x_38,

                                                              (x_36,

                                                               x_37))
-}
                             where ~(Nop) = x
                                   ~(Trap) = x
                                   ~(AddU x_30 x_31 x_32) = x
                                   ~(And x_33 x_34 x_35) = x
                                   ~(Div x_36 x_37 x_38) = x

-----------------------------------------------------------------------------------------------------------------------------

[Haskell-cafe] Strange problem with type classes (ghc 6.8.2 looks allright and ghc 6.10.1 doesn't).

Serguey Zefirov