search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
77 stars 18 forks source link

pretty not handling UnderAppliedCon #8

Closed ysangkok closed 3 years ago

ysangkok commented 3 years ago

Compiling elab-util with an idris2 commit from today, I get this error:

 % idris2 --build elab-util.ipkg
1/4: Building Language.Reflection.Pretty (src/Language/Reflection/Pretty.idr)
Error: pretty is not covering.

src/Language/Reflection/Pretty.idr:238:1--245:39
 238 | export
 239 | Pretty DotReason where
 240 |   pretty NonLinearVar   = "NonLinearVar"
 241 |   pretty VarApplied     = "VarApplied"
 242 |   pretty NotConstructor = "NotConstructor"
 243 |   pretty ErasedArg      = "ErasedArg"

Missing cases:
    pretty UnderAppliedCon
ysangkok commented 3 years ago

Adding the case seems to work, but I dunno if it breaks any assumptions. I guess it shouldn't since the Pretty instance is probably only for debugging...

stefan-hoeck commented 3 years ago

Thanks. This should be fixed with the latest commit.