:elab REPL asks intros for implicit arguments

[stop-cran]

It was noticed a different behavior of REPL and the compiler regarding Elab proofs - REPL asks intro for implicit arguments, whereas the compiler does not. Hence, proofs generated by :elab REPL command does not work if written in a file. Here's a simple example:

module Main

import Pruviloj.Core
import Pruviloj.Induction
import Language.Reflection.Elab

total
reflTest : (x : a) -> x = x
reflTest = ?h

Steps to Reproduce

Repeat REPL commands below:

ElabDoesNotWork>idris Main.idr -p pruviloj
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.0-git:fc3492474
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.h
*Main> :elab h

----------                 Goal:                  ----------
{hole_0} : (a : Type) -> (x : a) -> x = x
-Main.h> intro `{{a}}

----------              Assumptions:              ----------
 a : Type
----------                 Goal:                  ----------
{hole_0} : (x : a) -> x = x
-Main.h> intro `{{x}}

----------              Assumptions:              ----------
 a : Type
 x : a
----------                 Goal:                  ----------
{hole_0} : x = x
-Main.h> reflexivity
h: No more goals.
-Main.h> :qed
Proof completed!
Main.h = %runElab (do intro `{{a}}
                      intro `{{x}}
                      reflexivity)

Enter the proof in a source file:

module Main

import Pruviloj.Core
import Pruviloj.Induction
import Language.Reflection.Elab

total
reflTest : (x : a) -> x = x
reflTest = %runElab (do intro `{{a}}
                        intro `{{x}}
                        reflexivity)

Try to compile it, see following error:

Type checking .\Main.idr
1.idr:9:12-11:36:
  |
9 | reflTest = %runElab (do intro `{{a}}
  |            ~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of reflTest with expected type
        (x : a) -> x = x

Can't use lambda here: type is a = a

Expected Behavior

The interactive proof assistant does not ask intros for implicit arguments, like the compiler.

Observed Behavior

The interactive proof assistant asks for intros for implicit arguments, e.g.:

*Main> :elab h


----------                 Goal:                  ----------
{hole_0} : (a : Type) -> (x : a) -> x = x
-Main.h> intro `{{z}}

----------              Assumptions:              ----------
 z : Type
----------                 Goal:                  ----------
{hole_0} : (x : z) -> x = x

Previously asked on StackOverflow (here I simplified the sample a bit): https://stackoverflow.com/q/52225319/2858407