metaborg/dynsem

Implicit coercion incorrectly chosen in reduction premise

Closed this issue · 0 comments

Given the following:

module trans/foo

signature
  sorts
    Statement
    V
    U
  constructors
    V: V
    U: U
    
  sort aliases
    Code = List(Statement)
    
  arrows
    Code --> V
    install-import(Statement) --> Code
    
    run-code(Code) --> U  

rules

  run-code(code) --> U()
  where
    code --> V().

An error is reported on the pattern match V() due to the wrong arrow being selected to reduce code -->.