Sort Unification for Subsort Relations in Modules

[WilfredTA]

Athena rejects the use of unifiable sorts constructed via subsorts when in the context of a module.

Below are two code snippets, identical except that the second code snippet defines the BTree and related code inside of a Tree module, while the first snippet is defined in the top level Athena context.

datatype (BTree T) :=
    null |
    (leaf T) |
    (root (BTree T) (BTree T))

domains Sort1, Sort2, Sort

subsorts (Sort1 Sort2) Sort

declare data1: Sort1
declare data2: Sort2

define tree1 := (leaf data1)
define tree2 := (leaf data2)
define tree := (root tree1 tree2)

module Tree {

  datatype (BTree T) :=
      null |
      (leaf T) |
      (root (BTree T) (BTree T))
  
  domains Sort1, Sort2, Sort
  
  subsorts (Sort1 Sort2) Sort
  
  declare data1: Sort1
  declare data2: Sort2
  
  define tree1 := (leaf data1)
  define tree2 := (leaf data2)
  define tree := (root tree1 tree2)
}

Example 1 runs without error, while evaluating example 2 will cause Athena to report the following problem:

Error: Unable to infer a sort for the term: 

(Tree.root (Tree.leaf Tree.data1)

           (Tree.leaf Tree.data2))

(Failed to unify the sorts Tree.Sort2 and Tree.Sort1.).