Assertion patterns are too permissive: only the type is checked

[yanok]

I don't know if it's really a concern, but starting from the Dependent variant we can define an equality type and prove things about equalities. Unfortunately, the way unification is currently defined allows proving injectivity for an arbitrary function and thus making the whole thing inconsistent.

Here is the code:

data Eq (a : Type) (x : a) (y : a) where
| Refl (a : Type) (x : a) : Eq a x x
end

let inj :
  (a : Type) ->
  (b : Type) ->
  (f : a -> b) ->
  (x : a) ->
  (y : a) ->
  (eq : Eq b (f x) (f y)) ->
  Eq a x y =
  \a -> \b -> \f -> \x -> \y -> \eq ->
  case y || eq
  motive (y' : a) || (eq' : Eq b (f x) (f y')) || Eq a x y'
  of
  | .x || Refl .b .(f x) -> Refl a x
  end
end

I would love to see any suggestion how to fix that.

PS It also type checks with Dependent.Monadic variant... It's not clear for me why as there is no unification involved...

[be5invis]

I do not think that the .(f x) part in Refl .b .(f x) is a valid pattern. This may be the problem.

[be5invis]

The f is not a constructor of b.

[yanok]

But it doesn't have to be. .(f x) is an assertion pattern, it can be any term, not just a constructor.
Anyway, if you don't like it, if we switch to DependentImplicit version, we can define Refl with all implicit arguments and it will go away:

data Eq {a : Type} (x : a) (y : a) where
| Refl {a : Type} {x : a} : Eq x x
end

let inj :
  {a : Type} ->
  {b : Type} ->
  (f : a -> b) ->
  (x : a) ->
  (y : a) ->
  (eq : Eq (f x) (f y)) ->
  Eq x y =
  \{a} -> \{b} -> \f -> \x -> \y -> \eq ->
  case y || eq
  motive (y' : a) || (eq' : Eq (f x) (f y')) || Eq x y'
  of
  | .x || Refl -> Refl
  end
end

I believe the root of the problem is the way application is processed by the unification: unify function, then unify argument. This is good to instantiate implicits but results in wrong equality constraints.

[BekaValentine]

I've clearly created a bug somehow :(

[be5invis]

@psygnisfive Idris' unifier has special case for injectivity: https://hackage.haskell.org/package/idris-1.0/docs/src/Idris-Core-Unify.html

[be5invis]

Also: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Injectivity

[be5invis]

Coq's: https://coq.inria.fr/faq#htoc49

[yanok]

Ok, doing some more research I think probably the root cause is not the unification. It seems like it's not even about injectivity, I can even prove any two elements of the same type are equal:

let stupid :
  (a : Type) ->
  (x : a) ->
  (y : a) ->
  Eq a x y =
  \a -> \x -> \y ->
  case x
  motive (x' : a) || Eq a x' y
  of
  | .y -> Refl a y
  end
end

I tried it with Dependent.Monadic, Dependent.Unification and DependentImplcit.Unification. Will likely also work for the later variants. I think the problem is the handling of assertion patterns: the type checker only checks it has the correct type, but other than that you can put absolutely anything there.

[yanok]

Ok, I think I've fixed both of these problems in my own fork. I'll do some more testing and try to do a backport if anybody is interested.

To fix the problem with unchecked assertion patterns we simply have to substitute meta variable instead of assertion term in the following pattern types, while collecting equations in the form (metavar, assertion term). By the end of pattern checking these equations should be trivially (without extending the substitution) solvable. This won't work for the Monadic version though...

To fix the problem with function injectivity I've changed meta variables to be of one of the two sorts, existential and constraint. Also I've changed Equation constructor to hold an extra flag saying if it's ok to use it for constraints or not. Then we only need to fix the equate function to always reset this flag in the App case and change meta variable we use for assertion patterns to be constraints. This way unification will be still able to pick up implicits from unifying function applications but it won't allow to extract x == y constraint from f x == f y. I'm still not sure if assertion patterns is the only place there meta variables should not be existential though...

[yanok]

Here is the PR: #4