-
Notifications
You must be signed in to change notification settings - Fork 368
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
Idris refuses to unify types it can already infer. #3205
Comments
There are two different Why the unification error is expected: Unification can't sort out that So we have to match against The issue with the missing cases: Putting the Idris has to break that case statement into a tree of individual steps. You can see the result by typing succElim (MkI (P Negative () (P s w i))) (MkI (P Negative () (P s' w' j))) prf = ...
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative x (P s' w' j))) prf = ?what I looked at the case tree and there was a lot of succElim (MkI (P Negative _ (P _ _ _))) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative x (P s' w' j))) prf = At the beginning it says The code can be made to work by replacing the succElim (MkI (P Negative () (P _ _ _))) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative () (P s' w' j))) prf = ... My questions:
|
On a tangent line, I'm curious, why I have to write |
Yeah, I missed that. In Idris we can often leave a case-alt out if it is not possible. (No valid constructor given the context.) So we can remove all of the void cases: succElim : (i, j : I) -> succ i = succ j -> i = j
succElim (MkI Z) (MkI Z) Refl = Refl
succElim (MkI (S s w i)) (MkI (S s w i)) Refl = Refl
succElim (MkI (P Zero () Z)) (MkI (P Zero () Z)) Refl = Refl
succElim (MkI (P Negative MkUnit (P s w i))) (MkI (P Negative (MkUnit) (P s' w' j))) prf = cong pred prf One weird thing though, I removed the definition of |
Source code reproducing the issue.
I'm trying to define integers as follows:
In the construction above, with
P
(pred) andS
(succ) constructors, we could normally have an infinity of possible representations for each number (P (S Z)
would be equivalent to justZ
etc.). To eliminate these constructions we assert that insideP
we can only find anotherP
orZ
, but notS
. The mechanism is this: withinS sign nonNeg i
sign
declares the sign ofi
, and thennonNeg
evaluates to()
if it's correct or toVoid
if it's not. Since we cannot constructVoid
, we cannot also construct a non-canonical integer. In other wordsnonNeg
serves as a witness that the construction is canonical. Analogical argument goes forP
.Problem:
In the last clause for
succElim
there is thisx
variable, which should obviously evaluate to()
as it does in other cases where we haveP Negative ...
construction, but for some reason Idris insists that it cannot unifyx
and()
. If I try to replacex
with()
, it sayssuccElim
is not covering:Still, when I leave it as is, it happily decides it must be
()
:But when I try to return
z
(which has the right type if you substitute()
forx
), it complains that it cannot unifyx
and()
. How do I make sense of it? Is it some quirk of the type-checker or simply a bug?The text was updated successfully, but these errors were encountered: