search

GrammaticalFramework / gf-core

Grammatical Framework core: compiler, shell & runtimes
https://www.grammaticalframework.org
Other
128 stars 35 forks source link

Bug in type checker with dependent types #33

Open daherb opened 5 years ago

daherb commented 5 years ago

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 commented 5 years ago

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?