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

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

ConstructorDoesNotFitInData error for record in Prop with Set fields · Issue #7707 · agda/agda · GitHub

1. When defining the existential as proposition:

{-# OPTIONS --prop #-}

record Ex {A : Set} (P : A → Prop) : Prop where
  field
    witness : A
    prf     : P witness

I get a universe error:

Constructor Ex.constructor of sort Set
does not fit into data type of sort Prop.
(Reason: Set is not less or equal than Prop)
when checking that the type A of an argument to the constructor
Ex.constructor fits in the sort Prop of the datatype.

I suppose Agda should not let this pass without restriction; the projections do not make sense and neither does eta.
However, I am not sure the error message is the good one.
A better error would point to the impossibility to have fields of sort Set in a record targeting Prop, and maybe suggest to write a data instead, which is accepted:

data ExD {A : Set} (P : A → Prop) : Prop where
  mk : (w : A) → P w → ExD P

1. Related, there is a weird error for the data if I change Set to Prop1:

data ExD {A : Prop1} (P : A → Prop) : Prop where
  mk : (w : A) → P w → ExD P

Constructor mk of sort Prop₁
does not fit into data type of sort Set.
(Reason: Set₁ is not less or equal than Set)
when checking that the type A of an argument to the constructor mk
fits in the sort Set of the datatype.

The problem with this message is that the sort of ExD is not Set but Prop.

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