Constraint solving in heterogenous situations

[GoogleCodeExporter]

module Solve where

data Bool : Set where
  true false : Bool

_and_ : Bool → Bool → Bool
true  and x = x
false and x = false

infixr 5 _∷_

data Foo : Bool → Set where
  []  : Foo true
  _∷_ : ∀ {b} (x : Bool) → Foo b → Foo (x and b)

Baz : Bool → Set
Baz true = Bool
Baz false = Foo false

data Bar : ∀ {b} → Foo b → Set where
  []  : Bar []
  _∷_ : ∀ {b} {foo : Foo b} {x} (g : Baz x) → (bar : Bar foo) → Bar (x ∷ foo)

foo : Foo false
foo = false ∷ true ∷ []

bar : Bar foo
bar = (false ∷ []) ∷ false ∷ [] -- ← is yellow

{-
_59 := _55 ∷ false ∷ [] [blocked by problem 75]
[75] ["apply" (_53 ∷ true ∷ [])] == ["apply" (false ∷ true ∷ [])] : Foo 
(_53 and (true and true)) → Set [blocked by problem 76]
[76] (_53 and (true and true)) = false : Bool
_54 := false ∷ [] :? Baz _53
-}

Here, the solver's equation 75 is blocked by 76, but 76 can't be solved in isolation, so things turn yellow. However, if the solver ignored 76 and unified _53 with false, then it could solve 76. Ulf and I spoke about it on
IRC and he said it might be possible to have the solver first check that the "shape" of things being unified in 75 could be checked to make sure the unification makes sense, then they could be unified, then 76 could be attempted.

Original issue reported on code.google.com by pumpkingod@gmail.com on 22 Sep 2011 at 3:33

[GoogleCodeExporter]

What's needed here is the heterogenous shape machinery we just implemented for unification.

Original comment by ulf.nor...@gmail.com on 22 Sep 2011 at 6:02

• Changed title: Constraint solving in heterogenous situations
• Changed state: Accepted
• Added labels: Priority-Medium, Type-Enhancement

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 22 Sep 2011 at 9:42

• Added labels: Meta

[GoogleCodeExporter]

Has this been implemented? The code typechecks with no unsolved metas on the dev. version of Agda.

Original comment by sanzhi...@gmail.com on 26 Jan 2015 at 4:12

[GoogleCodeExporter]

No, this has not been implemented. However, the occurs check was strengthened. Also, this might be working due to bug #1258.

Original comment by andreas....@gmail.com on 26 Jan 2015 at 4:49

[GoogleCodeExporter]

This is a better test case then:

module Solve where

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

data Bool : Set where
  true false : Bool

_and_ : Bool → Bool → Bool
true  and x = x
false and x = false

infixr 5 _∷_

data Foo : Bool → Set where
  []  : Foo true
  _∷_ : ∀ {b} (x : Bool) → Foo b → Foo (x and b)

foo : let C = _ in (C ∷ []) ≡ (false ∷ [])
foo = refl

Original comment by sanzhi...@gmail.com on 27 Jan 2015 at 9:43

[andreasabel]

For the new example I get:

_25 : Bool 
_30 : Foo (_25 and true) 

Failed to solve the following constraints:
  _30 := false ∷ [] [blocked on problem 32]
  [32, 33] false = _25 and true : Bool

Could the proposal be fleshed out to see what it takes to implement this?

[vlopezj]

The test case given in #470 (comment) seems to type-check at least since commit ba4354f.

[gallais]

Can you please add it to the test suite?