Skip to content
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

Unification does not take into account the fact that types can be rewritten #1663

Closed
guillaumebrunerie opened this issue Sep 23, 2015 · 6 comments
Assignees

Comments

@guillaumebrunerie
Copy link
Contributor

@guillaumebrunerie guillaumebrunerie commented Sep 23, 2015

The code below gives the following error:

(base == base) !=< (PathOver _97 loop _99 _99) of type Set
when checking that the expression loop has type
PathOver _97 loop _99 _99

It works if we add {P = λ _ → Circle} at the last line, and it also works when using C-c C-Space to put loop (but then it doesn’t work when we reload the file).
The problem is that when trying to unify base == base and PathOver _97 loop _99 _99, agda doesn’t think about the fact that PathOver _97 loop _99 _99 could be rewritten to base == base using PathOver-rewr. When using C-c C-Space, agda already figured out that _97 must be constant, hence it works.

For now I’ve been able to work around it by putting the implicit arguments where needed, but it’s a bit annoying at times, especially given that C-c C-Space accepts it, because then I need to figure out which implicit argument is needed where.

{-# OPTIONS --without-K --rewriting #-}

postulate
  _↦_ :  {i} {A : Set i}  A  A  Set i
  idr :  {i} {A : Set i} {a : A}  a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

PathOver :  {i j} {A : Set i} (B : A  Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y)  Set j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

postulate
  PathOver-rewr :  {i j} {A : Set i} {B : Set j} {x y : A} (p : x == y) (u v : B) 
    (PathOver (λ _  B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-rewr #-}

ap :  {i j} {A : Set i} {B : A  Set j} (f : (a : A)  B a) {x y : A}
   (p : x == y)  PathOver B p (f x) (f y)
ap f idp = idp


postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ {i} {P : CircleSet i} (base* : P base) (loop* : base* == base* [ Ploop ])
 where
  postulate
    Circle-elim : (x : Circle)  P x
    Circle-base-β : Circle-elim base ↦ base*
    {-# REWRITE Circle-base-β #-}
    Circle-loop-β : ap Circle-elim loop ↦ loop*
    {-# REWRITE Circle-loop-β #-}

idCircle : Circle  Circle
idCircle = Circle-elim base loop
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Sep 23, 2015

Well, we could postpone constraint solving instead of failing in all situations where there possibly could be a rewrite rule that could fire, but I'm afraid this will result in a LOT of yellow and basically make the constraint solver useless. Maybe there is something smarter that we could do, but I don't see it immediately.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 15, 2015

On second thought, the problem seems to be that the non-linear matcher doesn't produce the correct blocking tags, i.e. it says ReallyNotBlocked when matching is in fact blocked on a meta. This then causes the unifier to assume that no meta instantiations will ever cause PathOver _97 loop _99 _99 to reduce, which in turn causes your error message. I'll look into improving the matching algoritm so it produces the proper blocking tags.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 15, 2015

@UlfNorell, is there any way to use Agda.TypeChecking.Free to get the MetaId of the meta to which a flexible variable is an argument? I need that information in order to generate the correct blocking tag. If there's nothing like that yet, would it be ok if I added it by adding an argument to the Flexible constructor of the FlexRig datatype?

@UlfNorell

This comment has been minimized.

Copy link
Member

@UlfNorell UlfNorell commented Oct 15, 2015

Knock yourself out. Though I guess it would be a (non-empty) list of MetaIds.

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Oct 15, 2015

Yes, please go ahead and refine the information about free variables. Should not be hard to do...

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 16, 2015

Ok, I did: f305ee9. There's still some places in the testing code where I didn't know how to generate a proper random list of MetaId's, so I just put an empty list instead.

One more thing I had to change to make the original example work was to disable injectivity for functions with rewrite rules (04b9603), because otherwise an equation like PathOver B p u v = (u == v) would be simplified to p = idp, which is of course no longer valid once you add the PathOver-rewr rule.

After that, I managed to get the example to work: 8aaf105. There's still some other places where the wrong blocking tags are generated, but at least this issue is fixed now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.