[Agda] generative thunk?

[Conor McBride]

Hi friends

I'm trying to do something quite involved, but I think the
problem I'm hitting boils down to some unwelcome generativity.

Let me fix my nonstandard ASCII terminology. (My current editor
displays all unicode characters as blanks. I rather like this
feature.)

postulate
   Lazy : forall {a} (A : Set a) -> Set a
   thunk : forall {a} {A : Set a} -> A -> Lazy A
   force : forall {a} {A : Set a} -> Lazy A -> A

{-# BUILTIN INFINITY Lazy #-}
{-# BUILTIN SHARP thunk #-}
{-# BUILTIN FLAT force #-}

OK, now I can write this...

put : (th : Set -> Lazy Set)(P : (Set -> Lazy Set) -> Set) ->
       P th -> P th
put th = \ P p -> p

...but if I want to be more specific, I hit trouble.

zut : (P : (Set -> Lazy Set) -> Set) ->
       P thunk -> P thunk
zut = put thunk  -- doesn't check

The error message

.Chat.thunk-6 P x != .Chat.thunk-8 x of type Lazy Set
when checking that the expression put thunk has type
(P : (Set → Lazy Set) → Set) →
P (.Chat.thunk-6 P) → P (.Chat.thunk-7 P)

suggests generativity issues, breaking stability under
substitution.

Amusingly,

fut : (P : (Set -> Lazy Set) -> Set) ->
       P _ -> P _
fut = put thunk

does typecheck.

It's a bit troubling.

Any clues as to what's going on?

Cheers

Conor