@type interface Equals<#x|> {}

@value interface Function<#y|#z> {}

concrete Value0<#t,#w> {
  #t allows #w
  #t requires Function<#t,#w>
  #w requires #t
  #w defines Equals<#w>
}

@value interface Value1 {
  refines Function<Value1,Value2>
}

concrete Value2 {
  refines Value3
  defines Equals<Value2>
}

concrete Value3 {
  refines Value1
}