#2478: Assertion failure in type checker
--------------------------------------------+-------------------------------
Reporter: simonpj | Owner: igloo
Type: merge | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.8.3
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: typecheck/should_compile/T2478 | Architecture: Unknown
Os: Unknown |
--------------------------------------------+-------------------------------
Old description:
> 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
> )
> )
> )
> }}}
New description:
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
)
)
)
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2478#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
