{-# LANGUAGE GADTs, DataKinds, StandaloneDeriving, FlexibleContexts, TemplateHaskell, TypeOperators, DeriveFunctor,DeriveFoldable,DeriveTraversable, DeriveGeneric, FlexibleInstances, PolyKinds #-}
module Types.TTT where
import Numeric.Natural
import Control.Lens
import Control.Monad
import Data.Comp.Multi
import Data.Comp.Multi.Show
import Data.Comp.Multi.Equality
import Data.Comp.Multi.Ordering
import Data.Comp.Multi.Derive
import Data.Comp.Ordering ()
import Data.Comp.Equality ()
import Data.Comp ()
import qualified Data.Comp.Derive as DCD
data PrimType = Int64 | Floating64 deriving (Eq, Ord)
data Variable ty where
Var :: String -> ty -> Variable ty
data CoreTT a i where
App :: a i -> a j -> CoreTT a i
Universe :: Natural -> CoreTT a Natural
data DevTT a i where
Hole :: Variable (a i) -> DevTT a i
data OptTT a i where
SSEVect :: a String -> OptTT a String
type Foo = DevTT :+: CoreTT :+: OptTT
$(derive [DCD.makeFunctor, DCD.makeFoldable, DCD.makeTraversable, DCD.makeShowF, DCD.makeEqF,
DCD.makeOrdF, DCD.smartConstructors, DCD.smartAConstructors]
[ ''Variable])
$(derive [makeHFunctor, makeHFoldable, makeHTraversable, makeShowHF, makeEqHF,
makeOrdHF, smartConstructors, smartAConstructors]
[ ''CoreTT, ''OptTT, ''DevTT])
Error messages:
src/Types/TTT.hs:37:5:
Could not deduce (KOrd Variable) arising from a use of ‘kcompare’
from the context (KOrd a)
bound by the type signature for
compareHF :: KOrd a => DevTT a i -> DevTT a j -> Ordering
at src/Types/TTT.hs:(37,5)-(39,39)
In the expression: kcompare x_asO6 y_asO7
In the first argument of ‘compdata-0.10:Data.Comp.Multi.Derive.Ordering.compList’, namely
‘[kcompare x_asO6 y_asO7]’
In the expression:
compdata-0.10:Data.Comp.Multi.Derive.Ordering.compList
[kcompare x_asO6 y_asO7]
src/Types/TTT.hs:37:5:
Could not deduce (KEq Variable) arising from a use of ‘keq’
from the context (KEq g)
bound by the type signature for
eqHF :: KEq g => DevTT g i -> DevTT g j -> Bool
at src/Types/TTT.hs:(37,5)-(39,39)
In the expression: (x_asNW `keq` y_asNX)
In the first argument of ‘and’, namely ‘[(x_asNW `keq` y_asNX)]’
In the expression: and [(x_asNW `keq` y_asNX)]
src/Types/TTT.hs:37:5:
Couldn't match expected type ‘K String i0’
with actual type ‘Variable (K String i)’
Relevant bindings include
x_asNN :: Variable (K String i) (bound at src/Types/TTT.hs:37:5)
showHF :: DevTT (K String) i -> K String i
(bound at src/Types/TTT.hs:37:5)
In the first argument of ‘unK’, namely ‘x_asNN’
In the expression: unK x_asNN
There was indeed a bug in the implementation. However, even after fixing it, I am afraid deriving Show, Eq and Ord is not possible for the DevTT type in the current setup.
Code:
Error messages: