Polymorphic constants crash Z3

[nikivazou]

Consider a polymorphic constant: constant poly: func(1, [A @(0)]).
In Z3 we will encode it monomorphised, i.e., declare-fun poly () (A Int). So, once we use it as A B, e.g., in {VV : A B | [ VV = poly ] } Z3 crashes with sort mismatch.

Is there a known way to address this problem (@ranjitjhala) ?
The full .fq file is below.

data B 0 = [
       | B {}
     ]
data A 1 = [
       | A {}
     ]

// in the smt poly is declared monororpshised to Int: 
// (declare-fun poly () (A Int))
constant poly: func(1, [A @(0)])


constraint:
  env []
  lhs {VV : A B | [ VV = poly ] }
  rhs {VV : A B | [ VV = poly ] }
  id 1 tag [1]

// so the above becomes `(= VV (as poly (A B)))` and crashed with 
// "invalid qualified identifier, sort mismatch"

[ranjitjhala]

This should get fixed in the same way we handle this test

• https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/tests/pos/undef00.fq
• https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/tests/pos/undef01.fq

but for some reason is not ...