If you try to check the following module, Mikan will panic.
moduleDisplayFormPanicwherepostulateA:Typebad:AmoduleBad(a:A)where{-# DISPLAY bad = a #-}-- Panic: unbound variable a (id: 8@ModuleNameHash-- 17663712797132180800)-- when checking the pragma DISPLAY bad = aThe culprit appears to be the call to inTopContext in checkDisplayPragma, which removes the a from the scope. This in turn causes the call to getVarInfo in exprToTerm to explode when it encounters the a.
If you try to check the following module, Mikan will panic.
```agda
module DisplayFormPanic where
postulate
A : Type
bad : A
module Bad (a : A) where
{-# DISPLAY bad = a #-}
-- Panic: unbound variable a (id: 8@ModuleNameHash
-- 17663712797132180800)
-- when checking the pragma DISPLAY bad = a
```
The culprit appears to be the call to `inTopContext` in `checkDisplayPragma`, which removes the `a` from the scope. This in turn causes the call to `getVarInfo` in `exprToTerm` to explode when it encounters the `a`.