id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
2478,Assertion failure in type checker,simonpj,,"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
                      )
                  )
       )
}}}",merge,closed,normal,6.8 branch,Compiler (Type checker),6.8.3,fixed,,,Unknown/Multiple,Unknown/Multiple,,Unknown,typecheck/should_compile/T2478,,,