Unsoundness in polymorphic subtying
CDuce says that the following simingly equal types are not equivalent (while they should be). Computing their differences yields a bogus type [ Empty]
(which should never be printed, since it is empty).
The problem is twofold:
- I think the pretty-printer is wrong and
[Empty]
is not displaying some variables that should be there (it appended before) - If the type really are equivalent (and not wrongly displayed as equivalent) then a bug lurks in the subtyping.
SIMPLIFY ERROR
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
Initial type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,-(X960,X958)(T,F,F)),F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>Simplified type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X1148,X1147)(F,F,-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F)))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
========
======== Simp\Initial (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(+(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)
(T,F,F),
F,F)),
F,
-(X960,X958)(F,F,
-(X1148,X1147)(F,F,
-(X1152,X1150)
(+(X1154,X1147)
(T,F,F),
F,F)))),
F,
-(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F))))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
======== Initial\Simp (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,
-(X960,X958)(+(X1148,X1147)(T,
=(X1152,X1150)
(F,
=(X1154,X1147)
(F,F,T),T),
F),
F,F)),
F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>