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
                      )
                  )
       )

[simonpj]

Fixed by

Fri Aug  1 13:22:23 BST 2008  simonpj@microsoft.com
  * Fix Trac #2478

Simon

[igloo]

We won't be releasing 6.8.4.