Proof is valid in elaborator shell but fails when inserted into the file

[michaelmesser]

Steps to Reproduce

Using Idris 1.1.1 Write this main.idr:

module Main

%language ElabReflection

a : Not (Int = String)
a = ?l

Run these commands

$ idris
*main> :load main.idr
Holes: Main.l
*main> :elab l

----------                 Goal:                  ----------
{hole_0} : (Int = String) -> Void
-Main.l> fill `(the (Not (Int = String)) (\Refl impossible))

----------                 Goal:                  ----------
{hole_0} : (Int = String) -> Void =?= the (Not (Int = String))
                                          (\lamp =>
                                             let scvar = lamp
                                             in case block in {val_0} at (input):1:40 lamp scvar)
-Main.l> solve
l: No more goals.
-Main.l> :qed
Proof completed!
Main.l = %runElab (do fill `(the (Not (Int = String)) (\Refl impossible))
                      solve)

Put the given script in the place of l to get:

module Main

%language ElabReflection

a : Not (Int = String)
a = %runElab (do
    fill `(the (Not (Int = String)) (\Refl impossible))
    solve)

Run these commands

*main> :load main.idr

Expected Behavior

It works fine

Observed Behavior

Type checking ./main.idr
main.idr:6:3:Incomplete term the (Not (Int = String))
                                 (\lamp => let scvar = lamp in scvar v2 lamp)
Holes: Main.a

[ahmadsalim]

Thanks for reporting the issue.