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

Type-checker fails unification unexpectedly for auto-implicit type #1875

Open
DrBearhands opened this issue Aug 29, 2021 · 3 comments
Open

Comments

@DrBearhands
Copy link
Contributor

Came across a situation I believe to be a bug, but might be my own error.

Steps to Reproduce

module Main

data PostS : (valType : Type) -> (stateType : Type) -> (valType -> stateType -> Type) -> Type where
  MkPostS
    :  (val : valType)
    -> (outState : stateType)
    -> {auto 0 prf : prop val outState}
    -> PostS valType stateType prop


data Foo = Bar | Baz

f : PostS Foo Foo Equal
f = MkPostS Bar Bar

Also asked on stackoverflow as I thought it may be my own error: https://stackoverflow.com/questions/68953988/idris2-compiler-tries-to-unify-type-values-unexpectedly

Expected Behavior

Compilation succeeds.

Observed Behavior

Error(s) building file [...]: While processing right hand side of f. When unifying Baz and Bar.
Mismatch between: Baz and Bar.

tests.HoareMonad2:14:5--14:20
 10 | 
 11 | data Foo = Bar | Baz
 12 | 
 13 | f : PostS Foo Foo (Equal)
 14 | f = MkPostS Bar Bar
          ^^^^^^^^^^^^^^^

MkPostS Baz Baz compiles correctly, as does MkPostS{prf=Refl} Bar Bar. Combinations of Bar and Baz correctly fail (even if given {prf=Refl}).

When replacing Foo with Nat, the value passed to MkPostS attempts (and fails to) match on 0.

@gallais
Copy link
Member

gallais commented Aug 29, 2021

This works so my guess is that the search is run in a different order
when using an auto-implicit and wrongly picks Refl {x = Baz} as the
proof.

  MkPostS                                                                         
    :  (val : valType)
    -> (outState : stateType)
    -> (prf : prop val outState)
    -> PostS valType stateType prop
 
 
data Foo = Bar | Baz
 
f : PostS Foo Foo Equal
f = MkPostS Bar Bar %search

@gallais
Copy link
Member

gallais commented Aug 29, 2021

Could be related to #1012 where auto was also too eager to pick a wrong solution.

@buzden
Copy link
Contributor

buzden commented Aug 30, 2021

This issue is definitely related to #814 since if you put the function f from the original example into a separate module, all typechecks finely.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants