New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heterogenous equality is crippled by the Bool /= Fin 2 fix #292

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 32 comments

Comments

Projects
None yet
2 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

ccasin observed that one can prove that Bool and Fin 2 are distinct
(see the #agda IRC channel logs,
http://agda.orangesquash.org.uk/2010/July.log):

  module foo where

  open import Data.Empty
  open import Data.Nat
  open import Data.Fin
  open import Data.Bool
  open import Data.Product
  open import Relation.Binary.HeterogeneousEquality hiding (subst)
  open import Relation.Binary.PropositionalEquality
  open import Relation.Nullary

  P : Set -> Set
  P S = Σ S (\s → s ≅ true)

  pbool : P Bool
  pbool = true , refl

  ¬pfin : ¬ P (Fin 2)
  ¬pfin ( zero , () )
  ¬pfin ( suc zero , () )
  ¬pfin ( suc (suc ()) , () )

  tada : ¬ (Bool ≡ Fin 2)
  tada eq = ⊥-elim ( ¬pfin (subst (\ S → P S) eq pbool ) )

Excerpt from the IRC channel logs:

  pigworker But here, Agda's dismissing a het equation between
            distinct value constructors of different types
  pigworker That's type-constructors-distinct by the back door, I
            suspect, at least for datatypes.
  Saizan    or maybe it's just ignoring the types and comparing the
            constructor names?
  pigworker Saizan: that's exactly what I think is happening

Original issue reported on code.google.com by nils.anders.danielsson on 4 Aug 2010 at 11:16

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

There are two ways to resolve this issue:
1 - make it not possible to prove Bool and Fin 2 distinct
2 - make it easier to prove Bool and Fin 2 distinct
Are there any problems with choosing the second option? This isn't
injective type constructors and I don't see an obvious reason why we
wouldn't want Bool and Fin 2 to be distinct (they clearly have different
elements).

Original comment by ulf.nor...@gmail.com on 13 Sep 2010 at 2:46

  • Changed state: Accepted
  • Added labels: Priority-Medium, Type-Defect
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I do not see a principal problem with 2, however at the moment things are 
inconsistent:
- If I slighly modify the code, I can prove Bool unequal Bool2, where true2, 
false2 : Bool2 (see file ..22.agda)
- However, if I rename the constructors to true, false : Bool2, then suddenly I 
cannot prove that Bool is unequal to Bool2 anymore (see other file).
So, at the moment Agda2 compares apples and oranges in certain situations. ;-)

Original comment by andreas....@gmail.com on 21 Sep 2010 at 12:30

Attachments:

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by nils.anders.danielsson on 4 Feb 2011 at 3:44

  • Added labels: Priority-High
  • Removed labels: Priority-Medium
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Andreas, BoolNotBool2 fails to type check due to ambiguity. If you
replace

  P : Set -> Set
  P S = Σ S (\s → s ≅ true)

with

  P : Set -> Set
  P S = Σ S (\s → s ≅ Bool.true),

then the code type checks.

Original comment by nils.anders.danielsson on 12 Feb 2011 at 6:27

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I see; so this was a false alarm.

Original comment by andreas....@gmail.com on 13 Feb 2011 at 12:04

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

> Are there any problems with choosing the second option?

Bool ≢ Fin 2 is inconsistent with the univalence axiom. (Note that the
example above relies on heterogeneous equality, which is also
inconsistent with the univalence axiom.)

I think we should choose the first option. Is it hard to implement?

Original comment by nils.anders.danielsson on 27 May 2011 at 12:39

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I looked into implementing the first option.  It seems that we need to avoid 
heterogeneous situations in unifyAtom, meaning that we should avoid comparing 
things at different type, creating constructorMismatches.  I manage to avoid 
some heterogeneous situations, like the one above, but this one is harder to 
avoid:

data D : Bool -> Set where
  tt : D true
  ff : D false

P : Set -> Set
P S = Σ S (\s → s ≅ tt)

pbool : P (D true)
pbool = tt , refl

¬pbool2 : ¬ P (D false)
¬pbool2 ( ff , () )

That should not emptyness-check either, because D true and D false are 
isomorphic!

Original comment by andreas....@gmail.com on 30 May 2011 at 8:23

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed, along with Issue 452.

Original comment by andreas....@gmail.com on 9 Sep 2011 at 4:48

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

As we have discussed, the current fix is a bit too restrictive.

Original comment by nils.anders.danielsson on 11 Sep 2011 at 2:43

  • Changed state: Accepted
  • Added labels: Milestone-2.2.12
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The fix makes us more restrictive that OTT which seems silly.

Original comment by ulf.nor...@gmail.com on 11 Sep 2011 at 2:48

  • Changed title: Heterogenous equality is crippled by the Bool /= Fin 2 fix
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I can look at it again tomorrow.

Original comment by andreas....@gmail.com on 11 Sep 2011 at 2:50

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed.  Unifier now can work in heterogeneous situations, as long as the two 
types at which it compares have same shape.

Original comment by andreas....@gmail.com on 13 Sep 2011 at 8:20

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 13 Sep 2011 at 8:20

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The code below should be accepted, shouldn't it?

module Bug where

data D : Set where
  d : D

postulate T : D → D → Set

data T′ (x y : D) : Set where
  c : T x y → T′ x y

F : D → D → Set
F x d = T′ x d

record [F] : Set where
  field
    x y : D
    f   : F x y

data _≡_ (x : [F]) : [F] → Set where
  refl : x ≡ x

Foo : ∀ {x} {t₁ t₂ : T x d} →
      record { f = c t₁ } ≡ record { f = c t₂ } → Set₁
Foo refl = Set

-- Bug.agda:24,5-9
-- unification failed due to postponed problems
-- when checking that the pattern refl has type
-- record { x = x; y = d; f = c t₁ } ≡
-- record { x = x; y = d; f = c t₂ }

-- Error from case-split command:
--
-- Bug.agda:24,10-16
-- Cannot decide whether there should be a case for the constructor
-- refl, since the unification gets stuck on unifying the inferred
-- indices [record { x = x; y = d; f = c t₁ }] with the expected
-- indices [record { x = x; y = d; f = c t₂ }]
-- when checking that the expression ? has type Set₁

Original comment by nils.anders.danielsson on 13 Sep 2011 at 2:56

  • Changed state: InfoNeeded
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

This latest bug is fixed.  Closing...

Original comment by andreas....@gmail.com on 14 Sep 2011 at 12:14

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

module Test where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  A : Set
  f : A → A

module Fails where

  -- Is it possible/safe to accept the definition of fails using some
  -- kind of shape-based unification?

  data C : A → Set where
    c : ∀ x → C (f x)

  record Box : Set where
    constructor box
    field
      a : A
      b : C a

  fails : ∀ {x₁ x₂} → box (f x₁) (c x₁) ≡ box (f x₂) (c x₂) → x₁ ≡ x₂
  fails refl = refl

module Workaround where

  data C : A → Set where
    c : ∀ x y → y ≡ f x → C y

  record Box : Set where
    constructor box
    field
      a : A
      b : C a

  works′ : ∀ {x₁ x₂ y₁ y₂ eq₁ eq₂} →
           box y₁ (c x₁ y₁ eq₁) ≡ box y₂ (c x₂ y₂ eq₂) → x₁ ≡ x₂
  works′ refl = refl

  works : ∀ {x₁ x₂} →
          box (f x₁) (c x₁ (f x₁) refl) ≡ box (f x₂) (c x₂ (f x₂) refl) →
          x₁ ≡ x₂
  works = works′

Original comment by nils.anders.danielsson on 15 Sep 2011 at 3:21

  • Changed state: InfoNeeded
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Another example:

module Test where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

-- Type checks if I is the empty record type.
-- record I : Set where

postulate
  I  : Set
  U  : I → Set
  El : ∀ {i} → U i → Set

mutual

  infixl 5 _▻_

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

  Type : Ctxt → Set
  Type Γ = Σ I (λ i → Env Γ → U i)

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (proj₂ σ γ)

postulate
  Γ : Ctxt
  σ : Type Γ

data D : Type (Γ ▻ σ) → Set where
  d : (τ : Type Γ) → D (proj₁ τ , λ γ → proj₂ τ (proj₁ γ))

record [D] : Set where
  constructor [d]
  field
    τ : Type (Γ ▻ σ)
    x : D τ

Foo : {τ₁ τ₂ : Type Γ} →
      [d] (proj₁ τ₁ , λ γ → proj₂ τ₁ (proj₁ γ)) (d τ₁) ≡
      [d] (proj₁ τ₂ , λ γ → proj₂ τ₂ (proj₁ γ)) (d τ₂) →
      Set₁
Foo refl = Set

Original comment by nils.anders.danielsson on 15 Sep 2011 at 8:09

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Also fixed these examples.  Keep it coming!

Original comment by andreas....@gmail.com on 15 Sep 2011 at 10:39

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

-- Another example:

module Bug where

postulate
  I     : Set
  i₁ i₂ : I

data D : I → Set where
  d₁ : D i₁
  d₂ : D i₂

data P : ∀ {i} → D i → Set where
  p₁ : P d₁
  p₂ : P d₂

-- The following definition is (and should be) rejected:
--
-- Foo : D i₁ → Set₁
-- Foo d₁ = Set
--
-- Error message:
--
-- Cannot decide whether there should be a case for the constructor
-- d₂, since the unification gets stuck on unifying the inferred
-- indices
--   [i₂]
-- with the expected indices
--   [i₁]
-- when checking the definition of Foo

-- However, I believe the following definition should be accepted:

Foo : P d₁ → Set₁
Foo p₁ = Set

-- It is not. Error message:
--
-- Cannot decide whether there should be a case for the constructor
-- p₂, since the unification gets stuck on unifying the inferred
-- indices
--   [{i₂}, d₂]
-- with the expected indices
--   [{i₁}, d₁]
-- when checking the definition of Foo
--
-- Here the shape-based machinery should kick in, right?

Original comment by nils.anders.danielsson on 18 Sep 2011 at 10:20

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

-- Presumably an instance of the same bug, but with another error
-- message:

module Bug where

postulate
  I     : Set
  i₁ i₂ : I

data D : I → Set where
  d₁ : D i₁
  d₂ : D i₂

data P : ∀ {i} → D i → Set where
  p₁ : P d₁

Foo : ∀ {i} (d : D i) → P d → Set₁
Foo d₁ _  = Set
Foo d₂ ()

-- P d₂ should be empty, but that's not obvious to me
-- when checking that the clause Foo d₂ () has type
-- {i : I} (d : D i) → P d → Set₁

Original comment by nils.anders.danielsson on 18 Sep 2011 at 10:20

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I fixed these examples without breaking any of the old test cases. I replaced a 
type error by checkEqualityHH (in the case of unifying two distinct function 
applications) and changed unification to start in the unifyConstructorArgs case 
(which is how we should treat the initial unification problem).

Original comment by ulf.nor...@gmail.com on 19 Sep 2011 at 7:19

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

.. oh, and Fixed

Original comment by ulf.nor...@gmail.com on 19 Sep 2011 at 7:24

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

-- Another example:

module Bug where

data ⊤ : Set where
  tt : ⊤

data D : (A : Set) → A → Set₁ where
  d : (A : Set) (x : A) → D A x

data P : (x : ⊤) → D ⊤ x → Set₁ where
  p : (x : ⊤) → P x (d ⊤ x)

Foo : P tt (d ⊤ tt) → Set₁
Foo (p .tt) = Set

-- Error message:
--
-- unification failed due to postponed problems
-- when checking that the pattern p .tt has type P tt (d ⊤ tt)

-- The error message above is not very good. If the code
--
-- Foo : P tt (d ⊤ tt) → Set₁
-- Foo x = {!x!}
--
-- is used instead, then an attempt to case split on x leads to the
-- following error message:
--
-- Cannot decide whether there should be a case for the constructor p,
-- since the unification gets stuck on unifying the inferred indices
-- [x', d ⊤ x'] with the expected indices [tt, d ⊤ tt]
-- when checking that the expression ? has type Set₁

Original comment by nils.anders.danielsson on 20 Sep 2011 at 9:34

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

This is not a bad error message, that is a serious bug!  Fixed now.  Example 
should check now (Issue292i).

Original comment by andreas....@gmail.com on 21 Sep 2011 at 2:47

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Great that you fixed the bug. Did you also fix the error message?

Original comment by nils.anders.danielsson on 21 Sep 2011 at 3:14

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Not yet...

Original comment by andreas....@gmail.com on 21 Sep 2011 at 3:29

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

And here's another bug for you. :)

module Bug where

postulate A : Set

data D : Set → Set where
  d₁ : D A
  d₂ : D (A → A)

data P : (B : Set) → B → D B → Set₁ where
  p₁ : (x : A)     → P A       x d₁
  p₂ : (f : A → A) → P (A → A) f d₂

Foo : (x : A) → P A x d₁ → Set₁
Foo x (p₁ .x) = Set

-- Cannot decide whether there should be a case for the constructor
-- p₂, since the unification gets stuck on unifying the inferred
-- indices
--   [A → A, f, d₂]
-- with the expected indices
--   [A, x, d₁]
-- when checking the definition of Foo

Original comment by nils.anders.danielsson on 21 Sep 2011 at 4:58

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed both comment 27 and the bad error message from comment 23. This time 
it'll stay fixed!

Original comment by ulf.nor...@gmail.com on 21 Sep 2011 at 6:41

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by nils.anders.danielsson on 24 Sep 2011 at 6:27

  • Added labels: Milestone-2.3.0
  • Removed labels: Milestone-2.2.12
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I really expect this to work:

postulate
  Val : Set
  app : Val → Val → Val

Rel = Val → Val → Set

Fam : Rel → Set1
Fam AA = ∀ {a a'} → .(AA a a') → Rel

Π : (AA : Rel) → Fam AA → Rel
Π AA FF g g' = ∀ {a a'} → .(a≼a' : AA a a') → FF a≼a' (app g a) (app 
g' a')

Π≅Π : {A' A : Rel}(A'≅A : A' ≅ A)
  {F : Fam A}{F' : Fam A'}(F≅F' : F ≅ F') →
  Π A F ≅ Π A' F'
Π≅Π refl refl = refl
{-
Refuse to solve heterogeneous constraint F :
.(A (_61 refl) (_62 refl)) → Val → Val → Set =?= F' :
.(A (_65 refl) (_66 refl)) → Val → Val → Set
when checking that the pattern refl has type F ≅ F'
-}

The problem seems to be the hidden arguments which are inserted after F and F'. 
 Otherwise there is no reason why we should be in a heterogeneous situation.

Original comment by andreas....@gmail.com on 5 Oct 2011 at 8:21

  • Changed state: Accepted

Attachments:

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Here is a shrunk case, with a different error message:

data _≅_ {A : Set1}(a : A) : {A' : Set1}(a' : A') → Set where
  refl : a ≅ a

postulate
  Val : Set
  app : Val → Val → Val

Pred = Val → Set

Fam : Pred → Set1
Fam A = ∀ {a} → A a → Pred

postulate
  Π : (A : Pred) → Fam A → Pred

Π≅Π' : (A : Pred)(F : Fam A)(F' : Fam A)(F≅F' : F ≅ F') →
  Π A F ≅ Π A F'
Π≅Π' A F F' refl = refl
{-
F {_38 A F F'} _ _ != F' {_38 A F F'} _ _ of type Set
when checking that the pattern refl has type
_≅_ {A (_38 A F F') → Pred} (F {_38 A F F'})
{A (_38 A F F') → Pred} (F' {_38 A F F'})
-}

Original comment by andreas....@gmail.com on 5 Oct 2011 at 8:37

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Mmh, the problem goes away if I manually eta-expand F and F':

  (F≅F' : (λ {a} Aa → F {a} Aa) ≅  (λ {a} Aa → F' {a} Aa))

So I guess, this is not a problem of the recent 292 fix, but a more general 
problem with unification, hidden arguments, and eta.

Closing.

Original comment by andreas....@gmail.com on 5 Oct 2011 at 8:59

  • Changed state: Fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment