Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[ fix #3672 ] prune unsolved metas that are not generalized over
- Loading branch information
Showing
6 changed files
with
226 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
{-# OPTIONS --allow-unsolved-metas #-} | ||
|
||
open import Agda.Builtin.Bool | ||
|
||
postulate | ||
A : Set | ||
|
||
F : Bool → Set | ||
F true = A | ||
F false = A | ||
|
||
data D {b : Bool} (x : F b) : Set where | ||
|
||
variable | ||
b : Bool | ||
x : F b | ||
|
||
postulate | ||
f : D x → (P : F b → Set) → P x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
Issue3655b.agda:19,7-34 | ||
Variable generalization failed. | ||
- Probable cause | ||
There were unsolved constraints that obscured the dependencies | ||
between the generalized variables. | ||
- Suggestion | ||
The most reliable solution is to provide enough information to make | ||
the dependencies clear, but simply mentioning the variables in the | ||
right order should also work. | ||
- Further information | ||
- Dependency analysis suggested this (likely incorrect) order: x b | ||
- After constraint solving it looks like x actually depends on b | ||
when checking that the expression D x → (P : F b → Set) → P x has | ||
type _9 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
{-# OPTIONS --allow-unsolved-metas #-} | ||
|
||
data C (A : Set) : Set where | ||
c : (x : A) → C A | ||
|
||
data D : Set where | ||
|
||
data E (A : Set) : Set where | ||
e : A → E A | ||
|
||
postulate | ||
F : {A : Set} → A → Set | ||
|
||
G : {A : Set} → C A → Set | ||
G (c x) = E (F x) | ||
|
||
postulate | ||
H : {A : Set} → (A → Set) → C A → Set | ||
f : {A : Set} {P : A → Set} {y : C A} → H P y → (x : A) → G y → P x | ||
g : {A : Set} {y : C A} {P : A → Set} → ((x : A) → G y → P x) → H P y | ||
|
||
variable | ||
A : Set | ||
P : A → Set | ||
x : A | ||
y : C A | ||
|
||
postulate | ||
h : {p : ∀ x → G y → P x} → (∀ x (g : G y) → F (p x g)) → F (g p) | ||
|
||
id : (A : Set) → A → A | ||
id _ x = x | ||
|
||
-- i : (h : H P y) → (∀ x (g : G y) → F (f h x g)) → F (g (f h)) | ||
-- i x y = id (F (g (f x))) (h y) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
{-# OPTIONS --allow-unsolved-metas #-} | ||
|
||
postulate | ||
A : Set | ||
|
||
data Unit : Set where | ||
unit : Unit | ||
|
||
F : Unit → Set | ||
F unit = A | ||
|
||
postulate | ||
P : {A : Set} → A → Set | ||
Q : ∀ {x} → F x → Set | ||
f : ∀ {x} {y : F x} (z : Q y) → P z | ||
|
||
variable | ||
x : Unit | ||
y : F x | ||
|
||
g : (z : Q y) → P z | ||
g z with f z | ||
... | p = p |