TOTBWF/tactic-haskell

`apply` can't handle typeclass methods

Opened this issue · 0 comments

TOTBWF commented

For example apply '(+) yields the error:

    Tactic Error: lookupVarType: Variable Type ClassOpI GHC.Num.+ (ForallT [KindedTV 
a_6989586621679035072 StarT] [AppT (ConT GHC.Num.Num) (VarT a_6989586621679035072)] 
(AppT (AppT ArrowT (VarT a_6989586621679035072)) (AppT (AppT ArrowT (VarT 
a_6989586621679035072)) (VarT a_6989586621679035072)))) GHC.Num.Num isn't implemented yet

Solving this could be a bit tricky, as we would need to work in an understanding of typeclass instances into things...