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 mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
