bug.agda

module bug where
open import Agda.Builtin.Equality
open import Data.Bool

module Acc
  (Level : Set)
  (_<_ : Level → Level → Set) where

  -- This definition somehow results in the arguments to U< being marked Nonvariant
  record Acc (k : Level) : Set where
    pattern
    inductive
    no-eta-equality
    constructor acc<
    field acc : ∀ {j} → j < k → Acc j

  -- This one doesn't
  -- data Acc (k : Level) : Set where
  --   acc< : (∀ {j} → j < k → Acc j) → Acc k

module CwFAcc
  (Level : Set)
  (_<_ : Level → Level → Set)
  (open Acc Level _<_)
  where

  postulate U' : ∀ k (U< : ∀ {j} → j < k → Set) → Set

  U< : ∀ {k} → Acc k → ∀ {j} → j < k → Set
  U< (acc< f) {j} j<k = U' j (U< (f j<k))

  module _ (i j k : Level) (accj : Acc j) (acck : Acc k) (i<j : i < j) (i<k : i < k) where
    wtf : U< accj i<j ≡ U< acck i<k
    wtf = refl
  -- compareElims
  --   a     = {k = k₁ : Level} →
  --           Acc k₁ → {j = j₁ : Level} → j₁ < k₁ → Set
  --   pols0 (truncated to 10) = Nonvariant Nonvariant Invariant Nonvariant