Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7853 below:

Subject reduction failure with instance constructors in parameterised modules · Issue #7853 · agda/agda · GitHub

Reported by @mietek and minimised further by me.

open import Agda.Builtin.Unit
it : ∀ {A : Set} {{_ : A}} → A
it {{a}} = a

-- The problem disappears if X is postulated instead
module _ (X : Set) where
  data U : X → Set where
    instance
      u : ∀ {x} → U x

  -- The problem disappears if this is used instead of an instance constructor
  -- instance
  --   u' : ∀ {x} → U x
  --   u' = u

  module _ (x : X) where
    f : U x → ⊤
    f u = tt

    _ = {! f it !} -- C-c C-x C-h C-c C-n: λ {_} → tt
    _ = {! f u  !} -- this is fine

With Agda 4930018, f it reduces to an implicit lambda despite not having a Π-type.

mietek4e554c4c and jespercockx

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4