Problems with inconsistent constraints (was internal error)

[m0davis]

I get an in internal error at src/full/Agda/TypeChecking/Substitute.hs:98 in this very complicated yet self-contained program, which I'll be happy to reduce to a small(er) test case if anyone asks. Please let me know if that would be helpful. (UPDATE: reduced test case coming soon.)

[UlfNorell]

See reply to mailing list: reduction to small test case is much appreciated.

[andreasabel]

There are unsolved metas before the crash happens. I wonder if the crash will still happen if these metas are solved. (In any case, Agda should not crash even with unsolved metas.)

After refining

  _≈_ : Ṗroperty ℓ 𝔒 → Ṗroperty ℓ 𝔒 → Set (𝔵 ⊔ 𝔬 ⊔ ℓ)
  _≈_ _ (∁ Q) = ∀ {x : 𝔛} {f : 𝔒 x} → Q {x} f

There are still unsolved metas in the type of fact5⋆.

Anyway, a smaller test case (with less unicode) would be greatly appreciated.

[m0davis]

@andreasabel Those unsolved metas only came about while I was trying to reduce the test case, so yeah, it'll still crash. In addition to making a small, less-unicode test case, I'll make sure there are no unsolved metas in the type.

[m0davis]

I stopped as soon as the program length (including the comment) was in the double-digits.

open import Agda.Primitive

infixr 5 _,_
record Pair
  {a} (A : Set a) {b} (B : Set b)
  : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B

data Constraint
  {a} {A : Set a} (x : A)
  : Set where
  instance _ : Constraint x

record Outer
  l {a} {A : Set a} (x : A)
  : Set (lsuc l) where
  constructor #
  field type : Set l

record Inner
  {l} {a} {A : Set a} (x : A) {{_ : Constraint x}} (outer : Outer l x)
  : Set l where
  field value : Outer.type outer

module Class
  {l} {a} {A : Set a} (x : A) (C : Set l)
  where
  class = Inner x (# C)
  method : {{_ : class}} → C
  method {{INSTANCE}} = Inner.value INSTANCE

module Beekeeper
  {i} {I : Set i}
  (A : I -> Set)
  (B : I -> Set)
  (x : I)
  = Class (x , A , B)
          (A x -> B x)

module Indexed
  {a b b?} {I : Set}
  {A : I -> Set a}
  (mkA : ∀ {x} -> A x)
  (B : I -> Set b)
  (toB : ∀ {x} -> A x -> B x)
  (B? : ∀ {x} -> B x -> Set b?)
  = Class ((λ {x} -> toB {x}) , (λ {x} -> B? {x}))
          (∀ {x} -> B? (toB (mkA {x})))

module Unindexed
  {a b}
  {A : Set a}
  (mkA : A)
  {B : Set b}
  (toB : A -> B)
  (B? : B -> Set)
  = Class (mkA , toB , B?)
          (B? (toB mkA))

module _
  {a b} {I : Set}
  {A : I -> Set a}
  {mkA : ∀ {x} -> A x}
  {B : I -> Set b}
  {toB : ∀ {x} -> A x -> B x}
  {B? : ∀ {x} -> B x -> Set}
  {{_ : Indexed.class mkA B toB B?}}
  where
  postulate
    instance iToUnindexed : ∀ {x} -> Unindexed.class (mkA {x}) toB B?

postulate
  I : Set

data A
  a (x : I)
  : Set a where
  mkA : A a x

record B
  b (x : I)
  : Set (lsuc b) where
  field ?? : Set b
open B public

postulate
  toB : ∀ {a b x} -> A a x -> B b x
  instance
    iIndexedAB : ∀ {a b} -> Indexed.class (mkA {a}) (B b) toB (B.??)
  b : Level
  x : I
  myB : B b x

error : myB .??
error = Beekeeper.method _ _ _ _ _
-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:98

Honestly, I stopped b/c I don't know what else I can do to simplify the problem.

[andreasabel]

Ok, great! I will do some further shrinking from here.

[andreasabel]

I got it a bit further, making the final B monomorphic and making a number of arguments visible.
The internal error is very brittle, many changes just turn it into a "No instance found" error.

open import Agda.Primitive

infixr 5 _,_

record Pair {a} (A : Set a) {b} (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B

-- If we turn Contraint, mkConstraint into postulate
-- we get "Failed to solve ... constraints" instead.

data Constraint {a} {A : Set a} (x : A) : Set where
  instance
    mkConstraint : Constraint x

record Outer l {a} {A : Set a} (x : A) : Set (lsuc l) where
  constructor mkOuter
  field
     type : Set l

record Inner {l} {a} {A : Set a} (x : A) {{_ : Constraint x}} (outer : Outer l x) : Set l where
  field
    value : Outer.type outer

module Class {l} {a} {A : Set a} (x : A) (C : Set l) where

  class = Inner x (mkOuter C)

  method : {{_ : class}} → C
  method {{INSTANCE}} = Inner.value INSTANCE

module Beekeeper {i} {I : Set i} (A : I → Set) (B : I → Set) (x : I)
  = Class (x , A , B) (A x → B x)

module Indexed
  a {I : Set}
  (A   : I → Set a)
  (mkA : ∀ (x : I) → A x)
  (B   : I → Set1)
  (toB : ∀ (x : I) → A x → B x)
  (B?  : ∀ (x : I) → B x → Set)
  = Class (toB , B?) (∀ x → B? x (toB x (mkA x)))

module Unindexed a (A : Set a) (mkA : A) (B : Set1) (toB : A → B) (B? : B → Set)
  = Class (mkA , toB , B?) (B? (toB mkA))

postulate
  instance
    iToUnindexed : ∀
      a (I : Set)
      (A   : I → Set a)
      (mkA : ∀ (x : I) → A x)
      (B   : I → Set1)
      (toB : ∀ (x : I) → A x → B x)
      (B?  : ∀ (x : I) → B x → Set)
      {{_ : Indexed.class a A mkA B toB B?}}
      (x : I) → Unindexed.class a (A x) (mkA x) (B x) (toB x) (B? x)

postulate
  I : Set

-- If we make A and mkA postulates, we get the "No instance" error instead
data A a : (x : I) → Set a where
  mkA : (x : I) → A a x

-- If we turn B and fld into postulates, we get the "No instance" error
record B : Set1 where
  field fld : Set
open B

postulate
  toB : ∀ {a : Level} (x : I) → A a x → B
  instance
    iIndexedAB : ∀ {a : Level} →
      Indexed.class a (A a) mkA (λ (x : I) → B) toB (λ (x : I) → fld)
  myB : B

error : fld myB
error = Beekeeper.method _ _ _ _

-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:98

The final message from Agda is:

conApp: constructor Issue2709a.A.mkA with fields [] projected by Issue2709a.B.fld

@UlfNorell : do you want to take over?

[UlfNorell]

Further simplification: getting rid of the module applications, exposing the instance goal that triggers the error, and specialising some arguments:

open import Agda.Primitive

infixr 5 _,_
postulate
  Pair : ∀ {a} (A : Set a) {b} (B : Set b) → Set (a ⊔ b)
  _,_  : ∀ {a} {A : Set a} {b} {B : Set b} → A → B → Pair A B

-- If we turn Contraint, mkConstraint into postulate
-- we get "Failed to solve ... constraints" instead.

data Constraint {a} {A : Set a} (x : A) : Set where
  mkConstraint : Constraint x

record Inner {l a} {A : Set a} (x : A) (_ : Constraint x) (C : Set l) : Set l where
  -- no-eta-equality  -- With no-eta we get "No instance" error
  field
    value : C

Class : ∀ {l a} {A : Set a} (x : A) (C : Set l) → Set l
Class x C = Inner x mkConstraint C

postulate
  I : Set

-- If we make A and mkA postulates, we get the "No instance" error instead
data A a : (x : I) → Set a where
  mkA : (x : I) → A a x

-- If we turn B and fld into postulates, we get the "No instance" error
record B : Set1 where
  field fld : Set
open B

postulate
  a : Level
  toB : (x : I) → A a x → B

postulate
  instance
    iToUnindexed : ∀
      {B   : I → Set1}
      {toB : ∀ (x : I) → A a x → B x}
      {B?  : ∀ (x : I) → B x → Set}
      {{_ : Class (toB , B?) (∀ x → B? x (toB x (mkA x)))}}
      {x : I} → Class (mkA x , toB x , B? x) (B? x (toB x (mkA x)))

    iIndexedAB : Class (toB , λ _ → fld) (∀ x → fld (toB x (mkA x)))

it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x

goal :
  let i = _
      I : Set i
      I = _
      A : I → Set
      A = _
      B : I → Set
      B = _
      x : I
      x = _
  in Class (x , A , B) (A x → B x)
goal = it

-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:95

[UlfNorell]

More simplification, splitting Class into two separate types.

open import Agda.Primitive

infixr 5 _,_
postulate
  Pair : ∀ {a} (A : Set a) {b} (B : Set b) → Set (a ⊔ b)
  _,_  : ∀ {a} {A : Set a} {b} {B : Set b} → A → B → Pair A B

-- If we turn Contraint, mkConstraint into postulate
-- we get "Failed to solve ... constraints" instead.

data Constraint {a} {A : Set a} (x : A) : Set where
  mkConstraint : Constraint x

postulate
  Inner : ∀ {l a b} {A : Set a} {B : Set b} (x : A) (y : B) → Constraint x → Set l → Set l

record Inner' {l a b c} {A : Set a} {B : Set b} {C : Set c} (x : A) (y : B) (z : C)
              (_ : Constraint (x , y , z)) (X : Set l) : Set l where
  -- no-eta-equality  -- With no-eta we get "No instance" error
  field
    value : X

Class : ∀ {l a b} {A : Set a} {B : Set b} (x : A) (y : B) (X : Set l) → Set l
Class x y X = Inner x y mkConstraint X

Class' : ∀ {l a b c} {A : Set a} {B : Set b} {C : Set c} (x : A) (y : B) (z : C) (X : Set l) → Set l
Class' x y z X = Inner' x y z mkConstraint X

postulate
  I : Set

-- If we make A and mkA postulates, we get the "No instance" error instead
data A a : (x : I) → Set a where
  mkA : (x : I) → A a x

-- If we turn B and fld into postulates, we get the "No instance" error
record B : Set1 where
  field fld : Set
open B

postulate
  a   : Level
  toB : (x : I) → A a x → B

postulate
  instance
    iToUnindexed : ∀
      {B   : I → Set1}
      {toB : ∀ (x : I) → A a x → B x}
      {B?  : ∀ (x : I) → B x → Set}
      {{_ : Class toB B? (∀ x → B? x (toB x (mkA x)))}}
      {x : I} → Class' (mkA x) (toB x) (B? x) (B? x (toB x (mkA x)))

    iIndexedAB : Class toB (λ _ → fld) (∀ x → fld (toB x (mkA x)))

it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x

goal =
  let i = _
      I : Set i
      I = A _ _
      A : I → Set
      A = _
      B : I → Set
      B = _
      x : I
      x = mkA _
  in it {A = Class' x A B (A x → B x)}

-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:95

Much simplified this is what happens:

_f     : A → Set
_Inst1 : Class A mkA _f (_f mkA)
_B     : Set
_g     : _B → Set

add constraint (1) A == _B
solve _f := _g : _B → Set   (*)
      _B := B, but don't recheck (1) yet
      _g := B.fld

crash on _Inst1 : Class A mkA B.fld (B.fld mkA)

It looks like the problematic step is (*), but I haven't quite figured out what exactly we're doing wrong. (If you're following along in the debug output, (*) is really _147 := _B?_163 _x_143 : _171 → Set.)

I confirmed that this isn't an instance issue. You can also trigger the problem by filling in the instance argument interactively (first iToUnindexed and then iIndexedAB).

Basically we have a failure of protecting ourselves from inconsistent constraints. This is more severe in a situation with instance arguments, since we are going to try some incorrect instance candidates before finding the right one, so we expect to encounter type errors also for correct programs.