Reification of constructors / Ill-formed with function type signature

[UlfNorell]

From arist...@gmail.com on April 17, 2012 03:53:50

I'm using Agda 2.3.0.1 with GHC 7.4.1 on OS X Lion.

The error message is (full version attached):

panic: error when printing error! /Users/aristid/Code/relational/Relational.agda:66,3-67,14 Panic: no such meta variable _592 when checking that the type ... of the generated with function is well-formed

The source code is (with the error occurring in the function Tuple at the very end) - I have no idea what is going wrong there, or what the error message might mean:

module Relational where

open import Function open import Function.Inverse hiding (∘) import Function.Equality as FE open import Data.Nat renaming (< to ℕ< ; compare to ℕ-compare) import Data.Nat.Properties as NP open import Relation.Binary open import Relation.Binary.PropositionalEquality using (≡ ; refl) import Data.AVL as AVL open import Data.Product open import Data.Maybe

module Inv = Function.Inverse module PE = Relation.Binary.PropositionalEquality

data Type : Set where top : Type

data Value : Type → Set where vtop : Value top

record IsKey (A : Set) : Set where field count : A ↔ ℕ

module Count = Inverse count

toℕ : A → ℕ toℕ = FE.⟨$⟩ Count.to

fromℕ : ℕ → A fromℕ = FE.⟨$⟩ Count.from

< : A -> A -> Set < = ℕ< on toℕ

isStrictTotalOrder : IsStrictTotalOrder ≡ < isStrictTotalOrder = record { isEquivalence = Setoid.isEquivalence (PE.setoid ); trans = trans; compare = compare; <-resp-≈ = PE.resp₂ } where module N = StrictTotalOrder NP.strictTotalOrder

      trans : Transitive _<_
      trans i<j j<k = N.trans i<j j<k

      compare : Trichotomous _≡_ _<_
      compare x y with N.compare (toℕ x) (toℕ y)
      compare x y | tri< a ¬b ¬c = tri< a (¬b ∘ PE.cong toℕ) ¬c
      compare x y | tri≈ ¬a b ¬c = tri≈ ¬a (Count.injective b) ¬c
      compare x y | tri> ¬a ¬b c = tri> ¬a (¬b ∘ PE.cong toℕ) c

strictTotalOrder : StrictTotalOrder strictTotalOrder = record { Carrier = A; ≈ = ≡; < = <_; isStrictTotalOrder = isStrictTotalOrder }

module Keyed (Key : Set) (isKey : IsKey Key) where open IsKey isKey

record AttrDef (key : Key) : Set where constructor adef field type : Type

AttrSet : Set AttrSet = AVL.Tree AttrDef isStrictTotalOrder

module AttrSet = AVL AttrDef isStrictTotalOrder

Tuple : AttrSet → Set Tuple attrs with AttrSet.headTail attrs ... | c = ?

module ℕ-Keyed = Keyed ℕ (record { count = Inv.id })

Attachment: err.txt

Original issue: http://code.google.com/p/agda/issues/detail?id=611

[UlfNorell]

From nils.anders.danielsson on April 17, 2012 02:15:58

This error seems to be fixed in the development version. Andreas?

Status: InfoNeeded
Owner: andreas....@gmail.com

[UlfNorell]

From arist...@gmail.com on April 17, 2012 16:09:15

Using darcs Agda (latest version, just compiled today), I still get the problem when using the 0.6 version of the standard library. Will check now if the problem disappears with the latest version of the standard library.

But with darcs Agda there is no "error printing error" anymore, just a regular, if incomprehensible, error message.

Namely:

/Users/aristid/Code/relational/Relational.agda:66,3-67,14 _592 Key isKey attrs x ≡ 593 Key isKey attrs x → suc (FE.⟨$⟩ (Inv.Inverse.to count) x₁) ≤ FE.⟨$⟩_ (Inv.Inverse.to count) (592 Key isKey attrs x) → suc (FE.⟨$⟩ (Inv.Inverse.to count) x₁) ≤ FE.⟨$⟩_ (Inv.Inverse.to count) (593 Key isKey attrs x) != {x y : Key} → x ≡ y → suc (FE.⟨$⟩ (Inv.Inverse.to count) x₁) ≤ FE.⟨$⟩ (Inv.Inverse.to count) x → suc (FE.⟨$⟩ (Inv.Inverse.to count) x₁) ≤ FE.⟨$⟩ (Inv.Inverse.to count) y because one is an implicit function type and the other is an explicit function type when checking that the type (attrs : AttrSet) → Maybe {.Level.zero} (Σ {.Level.zero} {.Level.zero} (Σ {.Level.zero} {.Level.zero} Key AttrDef) (λ x → AVL.Tree {.Level.zero} {.Level.zero} {.Level.zero} {Key} AttrDef {λ x₁ y → suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) x₁) ≤ FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) y} (record { isEquivalence = record { refl = λ {.x} → refl {} {} {}; sym = PE.sym {.Level.zero} {Key}; trans = PE.trans {.Level.zero} {Key} }; trans = λ {i} {j} {k} i<j j<k → .Data.Nat..trans {suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) i)} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} i<j (.Data.Nat..trans {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} {suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j)} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} (NP.≤-step {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} (.Data.Nat..refl′ {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j} (refl {} {} {}))) (.Data.Nat..trans {suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) j)} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} j<k (.Data.Nat..refl′ {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} {FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) k} (refl {} {} {})))); compare = λ x₁ y → .Relational.IsKey..with-116 {Key} isKey x₁ y (.Data.Nat.Properties..with-341 (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) x₁) (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) y) (ℕ-compare (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) x₁) (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) y))); <-resp-≈ = , {} {} {} {} (λ {x₁} → PE.subst {.Level.zero} {.Level.zero} {Key} (λ y → suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) x₁) ≤ FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) y)) (λ {y} → PE.subst {.Level.zero} {.Level.zero} {Key} (λ x₁ → suc (FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) x₁) ≤ FE.⟨$⟩ {} {} {} {} {} {} (Inverse.to {} {} {} {} {} {} (IsKey.count {} isKey)) y)) }))) → Set of the generated with function is well-formed

[UlfNorell]

From arist...@gmail.com on April 17, 2012 16:21:37

Same with the darcs version of the standard library. But that's presumably not an Agda bug, but a bug in my program that I just don't understand, right?

[UlfNorell]

From arist...@gmail.com on April 17, 2012 16:52:14

OK, I have been able to minimise the testcase to just a few lines of code, with the same error message:

module Minimal611 where

open import Data.Nat import Data.Nat.Properties as NP open import Relation.Binary import Data.AVL as AVL

data Type : Set where top : Type

record AttrDef (key : ℕ) : Set where constructor adef field type : Type

AttrSet : Set AttrSet = AVL.Tree AttrDef (StrictTotalOrder.isStrictTotalOrder NP.strictTotalOrder)

module AttrSet = AVL AttrDef (StrictTotalOrder.isStrictTotalOrder NP.strictTotalOrder)

Tuple : AttrSet → Set Tuple attrs with AttrSet.headTail attrs ... | c = ?

[UlfNorell]

From nils.anders.danielsson on April 18, 2012 01:55:11

As far as I can tell you are abstracting over a term which does not exist in the goal or context, and yet the with function's type signature is ill-formed. This looks like a bug.

Summary: Ill-formed with function type signature
Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Defect Priority-High

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 06:23:44

In Minimal611, this error seems to involve the type of

      .Relation.Binary.PropositionalEquality.Core.subst {.Level.zero}
      {.Level.zero} {ℕ} (_≤_ (suc x₁))

once with implicit arguments inserted, once without.

.Relation.Binary.Core.Dummy.≡ (_54 attrs x) (_55 attrs x) → suc x₁ ≤ _54 attrs x → suc x₁ ≤ 55 attrs x != {x y : ℕ} → .Relation.Binary.Core.Dummy.≡_ x y → suc x₁ ≤ x → suc x₁ ≤ y because one is an implicit function type and the other is an explicit function type

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 06:37:00

Here are the involved types of the std-lib

Respects : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set P Respects ∼_ = ∀ {x y} → x ∼ y → P x → P y

Respects₂ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set P Respects₂ ∼ = (∀ {x} → P x Respects ∼) × (∀ {y} → flip P y Respects ∼_)

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 06:38:25

Labels: With

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 06:51:14

The error is reproducible if one types the generated with-function type into Agda:

module Minimal611 where

import Level open import Data.Maybe open import Data.Product open import Relation.Binary.PropositionalEquality

open import Data.Nat import Data.Nat.Properties as NP open import Relation.Binary import Data.AVL as AVL

data Type : Set where top : Type

record AttrDef (key : ℕ) : Set where constructor adef field type : Type

AttrSet : Set AttrSet = AVL.Tree AttrDef (StrictTotalOrder.isStrictTotalOrder NP.strictTotalOrder)

module AttrSet = AVL AttrDef (StrictTotalOrder.isStrictTotalOrder NP.strictTotalOrder)

bla : Set1 bla = (attrs : AttrSet) → Maybe {Level.zero} (Σ {Level.zero} {Level.zero} (Σ {Level.zero} {Level.zero} ℕ AttrDef) (λ x → AVL.Tree {Level.zero} {Level.zero} {Level.zero} {ℕ} AttrDef {λ m → ≤ (suc m)} (record { isEquivalence = record { refl = λ {x} → refl {} {} {}; sym = sym {Level.zero} {ℕ}; trans = trans {Level.zero} {ℕ} }; trans = λ {i} {j} {k} i<j j<k → ?; compare = λ m n → ?; <-resp-≈ = , {} {} {} {} (λ {x₁} → subst {Level.zero} {Level.zero} {ℕ} (≤_ (suc x₁))) (λ {y} → subst {Level.zero} {Level.zero} {ℕ} (λ x₁ → suc x₁ ≤ y)) }) )) → Set

However, if I remove the four {} arguments to ,_ (line -4) then the error goes away.

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 06:52:48

One question is: Why does reify introduce these underscores for the parameters of constructors in the first place?

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 07:00:22

I think I found the culprit in Term.hs

-- | Check the type of a constructor application. This is easier than -- a general application since the implicit arguments can be inserted -- without looking at the arguments to the constructor. checkConstructorApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term checkConstructorApplication org t c args | hiddenArg = fallback | otherwise = do ...

-- Check if there are explicitly given hidden arguments,
-- in which case we fall back to default type checking.
-- We could work harder, but let's not for now.
hiddenArg = case args of
  Arg Hidden _ _ : _ -> True
  _                  -> False

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 09:26:45

The bug disappeared as I made checkConstructorApplication smarter. fallback is no longer invoked when the parameters to are a constructor are just underscores.

Still, the question is why reify introduces these underscores.

Also, why did these underscores cause the bug.

Status: Started

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 14:01:44

Here is a tiny testcase:

T : Bool -> Set T true = {x : Bool} -> Nat T false = {x : Bool} -> Bool

data D (b : Bool) : Set where c : T b -> D b

d : D false d = c {_} true

Fails with current agda.

checkHeadApplication inferred c : {b : Bool} → T b → D b checkHeadApplication inferred true : Bool checking Bool ?<= (T _21) checking D _21 ?<= D false /Users/abel/cover/alfa/Agda2-clean/test/succeed/ Issue611 .agda:18,11-15 Bool !=< ({Bool} → Bool) of type Set when checking that the expression true has type T false

Basically, inference does not produce the correct result type for true, since in fact

{x} -> true

is what really should be looked at.

My fix works for this case since it basically considers

d = c true

instead.

A fundamental problem with inference of hidden functions remains. One fix would be to make type conversion into type cast, i.e., when checking

true : Bool ?<= {Bool} -> Bool

a hidden lambda would be inserted, returning {_} -> true.

This is related to coercive subtyping.

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 14:11:17

I pushed my fix. Some fundamental clarifications remain necessary.

Summary: Reification of constructors / Inference of hidden functions / Ill-formed with function type signature
Owner: andreas....@gmail.com

[UlfNorell]

From andreas....@gmail.com on April 18, 2012 14:13:18

Labels: -Priority-High Priority-Medium

[UlfNorell]

From andreas....@gmail.com on April 19, 2012 00:07:46

When we switch from constructor to postulate, the problem with hidden abstractions becomes apparent:

T : Bool → Set T true = {x : Bool} → Bool T false = {x : Bool} → Bool

postulate D : Bool → Set c : (b : Bool) → T b → D b

d : D false d = c _ true

The type is not pushed in, thus instead of checking true against T false, the type of true is inferred to Bool, instead of being checked against {Bool} -> Bool. Later, conversion complains:

Bool !=< ({Bool} → Bool) of type Set when checking that the expression true has type T false

Since there is a value for _ that makes the expression type-check, this may not be an error.

A fix would be switching to coercive subtyping, i.e., the subtyping test modifies the term whose inferred type is compared to its ascribed type. Then, unsolved constraints are like postponed type checking problems.

Cc: ulf.nor...@gmail.com
Labels: Conversion

[UlfNorell]

From andreas....@gmail.com on April 21, 2012 01:53:32

I modified reification of constructors such that now the parameter arguments are skipped.

Coercice subtyping is a bigger issue. Should be separated from this bug report.

Closing

Summary: Reification of constructors / Ill-formed with function type signature
Status: Fixed
Labels: -Conversion