Bug in type checker with dependent types

[daherb]

Hi, if I have an abstract syntax like

abstract Equal = {
  cat Num;
      IsEqual Num Num ;
  fun
    z : Num ;
    s : Num -> Num ;
    equal : (n : Num) -> IsEqual n n ;
}

and generate trees of the category IsEqual with meta-variables, I get the following result as expected

Equal> gt -cat="IsEqual ? z"
equal z

but if I change the position of the question mark I get the following error:

Equal> gt -cat="IsEqual z ?"
src/runtime/haskell/PGF/TypeCheck.hs:(178,35)-(179,54): Non-exhaustive patterns in case

[heatherleaf]

Looking into the source code:

getMeta :: MetaId -> TcM s (MetaValue s)
getMeta i = TcM (\abstr k h ms -> case IntMap.lookup i ms of
                                    Just mv -> k mv ms)

So, the typechecker tries to lookup a metavariable which it has not seen yet. @krangelov any ideas about this?