[Agda] Modeling reflective languages

[Alan Jeffrey]

Hi everyone,

I've been working with models of class-based languages with reflection 
recently.  A stripped down version is:

module Bug where

data PreModel {C : Set} (M : C → Set) : Set → Set where
   model : (c : C) → (PreModel M (M c))

Model : {C : Set} → (C → Set) → Set
Model {C} M = PreModel M C

reflect : {C : Set} → {M : C → Set} → (Model M) → C
reflect (model c) = c

The idea being that (model c : Model M) is a solution to:

   M : (M c) → Set
   c : (M c)

Unfortunately, Agda 2.2.6 responds with:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Telescope.hs:51

I reported this at http://code.google.com/p/agda/issues/detail?id=280

There's an easy fix, which is:

reflect : {C X : Set} → {M : C → Set} → (PreModel M X) → C
reflect (model c) = c

but the internal error makes me suspect that not many other Agda users 
have gone down this road.  Is there an better model I should be used for 
reflection?  I'd like to avoid using propositional equality as the means 
of stating the recursive equation, since the intension is to provide a 
model of reflection which non-type-theorists can follow.

A.