Assertion failure in type checker
Doaitse reports: It appears we ran into a bug which has been reported before. We ran into it in a desperate attempt to follow some suggestions made by referees to simplify our library for transformations of typed abstract syntax . Unfortunately the paper was rejected, but we decided to try once more. The program fragment is probably erroneous, and we know how to repair it by taking away a context constraint and putting in some kind annotations, but we thought it would be good to report it anyway.
loeki:Desktop doaitse$ ghci Bug.hs
GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Var/Type length mismatch:
[]
[env2{tv aul} [tau]]
Ok, modules loaded: Main.
Code is
data Ref a env where
Zero :: Ref a (a,env')
Suc :: Ref a env' -> Ref a (x,env')
newtype T e s
= T {unT :: forall x . Ref x e -> Ref x s}
class Extendable state t where
extend :: t a s -> state t s env -> state t s (a,env)
data Extendable st t => Trafo st t a b =
Trafo ( forall env1 s. a s -> st t s env1 -> TrafoE st t a b env1 s )
data Extendable st t => TrafoE st t a b env1 s =
forall env2 . TrafoE
(T env2 s -> (b s, T env1 s , st t s env2))
newSRef :: (Extendable env t) => Trafo env t (t a) (Ref a)
newSRef
= Trafo
(\ta env ->
TrafoE
(\(T tr) ->
( tr Zero
, T (tr . Suc)
, extend ta env
)
)
)