diff --git a/src/Refinements-Parsing/FQParser.class.st b/src/Refinements-Parsing/FQParser.class.st
index bb37cd83a..fe9df71c2 100644
--- a/src/Refinements-Parsing/FQParser.class.st
+++ b/src/Refinements-Parsing/FQParser.class.st
@@ -29,6 +29,7 @@ FQParser >> def [
 	^ self fixpoint
 	/ self constraint
 	/ self iBind
+	/ data
 	/ 'everything else' asParser
 ]
 
diff --git a/src/Refinements-Parsing/FixpointParser.class.st b/src/Refinements-Parsing/FixpointParser.class.st
index 5418e5798..7a25bb104 100644
--- a/src/Refinements-Parsing/FixpointParser.class.st
+++ b/src/Refinements-Parsing/FixpointParser.class.st
@@ -5,7 +5,8 @@ Class {
 		'sort',
 		'sortArg',
 		'funcSort',
-		'pred'
+		'pred',
+		'data'
 	],
 	#category : #'Refinements-Parsing'
 }
@@ -20,6 +21,34 @@ FixpointParser class >> upperId [
 	^(#uppercase asParser, (#word asParser / $_ asParser) star) flatten
 ]
 
+{ #category : #grammar }
+FixpointParser >> data [
+	^'data' asParser trim,
+	self fTyCon trim,
+	PPParser decimalNat trim,
+	$= asParser trim,
+	($| asParser trim, self dataCtor trim ==> #second) star brackets
+		==> [ :x | DataDecl
+			ddTyCon: x second
+			ddVars: x third
+			ddCtors: x fifth ]
+]
+
+{ #category : #grammar }
+FixpointParser >> dataCtor [
+	^FixpointParser upperId trim,
+	(self dataField commaSeparated optional ==> [ :x | x ifNil: [#()] ifNotNil: [x] ]) braces
+	==> [ :x | DataCtor dcName: x first dcFields: x second ]
+]
+
+{ #category : #grammar }
+FixpointParser >> dataField [
+	^ FixpointParser upperId trim,
+	$: asParser trim,
+	sort
+	==> [ :x | DataField dfName: x first dfSort: x last ]
+]
+
 { #category : #grammar }
 FixpointParser >> fTyCon [
 	^ ('Int' asParser ==> [ :x | Int tyCon ])
diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st
index c0d34494c..f621fd9f9 100644
--- a/src/Refinements-Parsing/NNFParser.class.st
+++ b/src/Refinements-Parsing/NNFParser.class.st
@@ -78,7 +78,7 @@ NNFParser >> hThing [
 		/ self fixpoint
 		/ define
 		" / match"
-		" / data"
+		/ data
 	) parens
 ]
 
diff --git a/src/Refinements-Tests/FQPosTest.class.st b/src/Refinements-Tests/FQPosTest.class.st
index bdc3f3d22..09247ae10 100644
--- a/src/Refinements-Tests/FQPosTest.class.st
+++ b/src/Refinements-Tests/FQPosTest.class.st
@@ -31,3 +31,24 @@ constraint:
   tag [1]
 '
 ]
+
+{ #category : #tests }
+FQPosTest >> testEqConstr1 [
+	self provePos: '
+data Thing 0 = [
+  | Cons {Head : int}
+]
+
+bind 0 a : {v: Thing | Bool true }
+bind 1 x : {v: Thing | Bool true }
+bind 2 y : {v: `a    | Bool true }
+
+constraint:
+  env [0; 1; 2]
+  lhs {v:int | x === y }
+  rhs {v:int | y === x }
+  id 1 tag []
+'.
+
+
+]
diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st
new file mode 100644
index 000000000..b76905faa
--- /dev/null
+++ b/src/Refinements/DataCtor.class.st
@@ -0,0 +1,75 @@
+"
+data DataCtor = DCtor
+  { dcName   :: !LocSymbol        -- ^ Ctor Name
+  , dcFields :: ![DataField]      -- ^ Ctor Fields
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+"
+Class {
+	#name : #DataCtor,
+	#superclass : #Object,
+	#instVars : [
+		'dcName',
+		'dcFields'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataCtor class >> dcName: dcName dcFields: dcFields [
+	^self basicNew
+		dcName: dcName;
+		dcFields: dcFields;
+		yourself
+]
+
+{ #category : #'SMT interface' }
+DataCtor >> apply: ts [ 
+	^DataCtor
+		dcName: dcName
+		dcFields: (dcFields collect: [ :field | field apply: ts ])
+]
+
+{ #category : #accessing }
+DataCtor >> dcFields [
+	^ dcFields
+]
+
+{ #category : #accessing }
+DataCtor >> dcFields: anObject [
+	dcFields := anObject
+]
+
+{ #category : #accessing }
+DataCtor >> dcName [
+	^ dcName
+]
+
+{ #category : #accessing }
+DataCtor >> dcName: anObject [
+	dcName := anObject
+]
+
+{ #category : #'SMT interface' }
+DataCtor >> declare: aMonomorphizedDataDecl in: γ [
+	aMonomorphizedDataDecl
+			declare: dcName
+			accessors: (dcFields collect: [ :field | field declarationAssociation: aMonomorphizedDataDecl in: γ ])
+]
+
+{ #category : #printing }
+DataCtor >> printOn: aStream [
+	aStream
+		nextPutAll: '↪';
+		nextPutAll: dcName;
+		nextPutAll: '('.
+	dcFields do:
+		[ :df | aStream nextPutAll: df dfName; nextPutAll: '::'. df dfSort printOn: aStream ]
+		separatedBy: [ aStream nextPutAll: ',' ].
+	aStream
+		nextPutAll: ')'
+]
+
+{ #category : #Symbolic }
+DataCtor >> symbol [
+	^dcName
+]
diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st
new file mode 100644
index 000000000..20ce9714a
--- /dev/null
+++ b/src/Refinements/DataDecl.class.st
@@ -0,0 +1,124 @@
+"
+data DataDecl = DDecl
+  { ddTyCon :: !FTycon            -- ^ Name of defined datatype
+  , ddVars  :: !Int               -- ^ Number of type variables
+  , ddCtors :: [DataCtor]         -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+"
+Class {
+	#name : #DataDecl,
+	#superclass : #Object,
+	#instVars : [
+		'ddTyCon',
+		'ddVars',
+		'ddCtors'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataDecl class >> ddTyCon: ddTyCon ddVars: ddVars ddCtors: ddCtors [
+	^self basicNew
+		ddTyCon: ddTyCon;
+		ddVars: ddVars;
+		ddCtors: ddCtors;
+		yourself 
+	
+]
+
+{ #category : #construction }
+DataDecl >> addToQuery: aNNFQuery [ 
+	aNNFQuery qData add: self
+]
+
+{ #category : #'SMT interface' }
+DataDecl >> apply: ts [
+	"Given type-parametrized receiver ...@(0)...@(1)...,
+	 and actual type parameters t₀, t₁, …, answer a DataDecl with
+	 all formal type parameters substituted: ...t₀...t₁... ." 
+	^DataDecl
+		ddTyCon: (ddTyCon apply: ts)
+		ddVars: 0
+		ddCtors: (ddCtors collect: [ :ctor | ctor apply: ts])
+]
+
+{ #category : #accessing }
+DataDecl >> ddCtors [
+	^ ddCtors
+]
+
+{ #category : #accessing }
+DataDecl >> ddCtors: anObject [
+	ddCtors := anObject
+]
+
+{ #category : #accessing }
+DataDecl >> ddTyCon [
+	^ ddTyCon
+]
+
+{ #category : #accessing }
+DataDecl >> ddTyCon: anObject [
+	ddTyCon := anObject
+]
+
+{ #category : #accessing }
+DataDecl >> ddVars [
+	^ ddVars
+]
+
+{ #category : #accessing }
+DataDecl >> ddVars: anObject [
+	ddVars := anObject
+]
+
+{ #category : #GT }
+DataDecl >> gtInspectorConstructorsIn: composite [
+	<gtInspectorPresentationOrder: 40>
+	^ composite fastList
+		title: 'Constructors';
+		display: [ ddCtors ]
+]
+
+{ #category : #'SMT interface' }
+DataDecl >> monomorphicDeclIn: γ [
+	| known |
+	known := [ Context readState: #knownMonomorphizedDecls ]
+		on: NoAnswer
+		do: [ :_ex | [ ^self monomorphicDeclIn: γ ] runReader: #knownMonomorphizedDecls initialState: Dictionary new ].
+	^known
+		at: ddTyCon symbol
+		ifAbsentPut: [
+			| mdd |
+			mdd := MonomorphizedDataDecl named: ddTyCon symbol encodeUnsafe.
+			known at: ddTyCon symbol put: mdd.
+			ddCtors do: [ :ctor | ctor declare: mdd in: γ ].
+			mdd
+		]
+
+
+	
+]
+
+{ #category : #printing }
+DataDecl >> printOn: aStream [
+	aStream nextPutAll: 'data '.
+	aStream nextPutAll: self ddTyCon symbol
+]
+
+{ #category : #Symbolic }
+DataDecl >> symbol [
+"
+instance Symbolic DataDecl where
+  symbol = symbol . ddTyCon
+"
+	^ddTyCon symbol
+]
+
+{ #category : #'SMT interface' }
+DataDecl >> z3sort: γ [
+	ddVars = 0 ifFalse: [ self error ].
+	^PreSort hotel
+		at: ddTyCon symbol
+		ifAbsentPut: [ (self monomorphicDeclIn: γ) create ]
+]
diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st
new file mode 100644
index 000000000..80a692e0e
--- /dev/null
+++ b/src/Refinements/DataField.class.st
@@ -0,0 +1,61 @@
+"
+data DataField = DField
+  { dfName :: !LocSymbol          -- ^ Field Name
+  , dfSort :: !Sort               -- ^ Field Sort
+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+
+"
+Class {
+	#name : #DataField,
+	#superclass : #Object,
+	#instVars : [
+		'dfName',
+		'dfSort'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+DataField class >> dfName: dfName dfSort: dfSort [
+	^self basicNew
+		dfName: dfName;
+		dfSort: dfSort;
+		yourself
+]
+
+{ #category : #'SMT interface' }
+DataField >> apply: ts [ 
+	| θ |
+	θ := Dictionary
+		newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]).
+	^DataField
+		dfName: dfName
+		dfSort: (dfSort apply: θ)
+]
+
+{ #category : #'SMT interface' }
+DataField >> declarationAssociation: aMonomorphizedDataDecl in: γ [
+
+	^dfName -> (dfSort monomorphicDeclIn: γ)
+]
+
+{ #category : #accessing }
+DataField >> dfName [
+	^ dfName
+]
+
+{ #category : #accessing }
+DataField >> dfName: anObject [
+	dfName := anObject
+]
+
+{ #category : #accessing }
+DataField >> dfSort [
+	^ dfSort
+]
+
+{ #category : #accessing }
+DataField >> dfSort: anObject [
+	dfSort := anObject
+]
diff --git a/src/Refinements/Equation.class.st b/src/Refinements/Equation.class.st
index f3364ba7b..42557b50b 100644
--- a/src/Refinements/Equation.class.st
+++ b/src/Refinements/Equation.class.st
@@ -38,7 +38,7 @@ mkEquation f xts e out = Equ f xts e out (f `elem` syms e)
 		yourself
 ]
 
-{ #category : #adding }
+{ #category : #construction }
 Equation >> addToQuery: aHornQuery [ 
 	aHornQuery qEqns add: self
 ]
diff --git a/src/Refinements/FApp.class.st b/src/Refinements/FApp.class.st
index 75dff07ff..2c57d6ae5 100644
--- a/src/Refinements/FApp.class.st
+++ b/src/Refinements/FApp.class.st
@@ -72,6 +72,26 @@ FApp >> hash [
 	^s hash
 ]
 
+{ #category : #hotel }
+FApp >> monomorphicDeclIn: γ [
+	"Like fappSmtSort but don't go all the way to Z3.
+	 Do we want to keep this layer?"
+	(s isKindOf: FTC) ifFalse: [ self error ].
+	s isSetCon ifTrue: [ self error ].
+	s isMapCon ifTrue: [ self shouldBeImplemented ].
+	s isBitVec ifTrue: [ self shouldBeImplemented ].
+
+	^(s maybeDataIn: γ)
+		ifNil: [ self error]
+		ifNotNil: [ :d |
+			| instance ct_ts ct ts |
+			ct_ts := self unFApp.  ct := ct_ts first.  ts := ct_ts allButFirst.
+			instance := d apply: (ts collect: [ :each | each z3sort: γ ]).
+			instance monomorphicDeclIn: γ
+			
+		]
+]
+
 { #category : #printing }
 FApp >> printOn: aStream [
 	aStream nextPutAll: '(FApp '.
diff --git a/src/Refinements/FInfo.class.st b/src/Refinements/FInfo.class.st
index b01507565..fb3192800 100644
--- a/src/Refinements/FInfo.class.st
+++ b/src/Refinements/FInfo.class.st
@@ -41,7 +41,7 @@ but at least textually consistent with LF.
 	quals := OrderedCollection new.
 	gLits := SEnv new.
 	kuts := Kuts new.
-	ddecls := OrderedCollection new.
+	ddecls := defs select: [ :def | def isKindOf: DataDecl ].
 	ae := AxiomEnv new.
 	options := QueryOptions new.
 ]
diff --git a/src/Refinements/FTC.class.st b/src/Refinements/FTC.class.st
index 8d40c2559..2c4bc09e5 100644
--- a/src/Refinements/FTC.class.st
+++ b/src/Refinements/FTC.class.st
@@ -52,8 +52,10 @@ FTC >> fappSmtSort: ts originalFApp: anFApp in: γ [
 	^(self maybeDataIn: γ)
 		ifNil: [ (FObj symbol: typeConstructor symbol) fappSmtSort: ts originalFApp: anFApp in: γ ]
 		ifNotNil: [ :d |
+			| instance |
 			d ddVars = ts size ifFalse: [ self error ].
-			d instantiateZ3Sort: (ts collect: [ :t | t z3sort: γ ])
+			instance := d apply: (ts collect: [ :t | t z3sort: γ ]).
+			instance z3sort: γ
 		]
 ]
 
diff --git a/src/Refinements/HCon.class.st b/src/Refinements/HCon.class.st
index e6f794deb..0dd39765d 100644
--- a/src/Refinements/HCon.class.st
+++ b/src/Refinements/HCon.class.st
@@ -21,7 +21,7 @@ HCon class >> symbol: sym sort: srt [
 		yourself 
 ]
 
-{ #category : #logic }
+{ #category : #construction }
 HCon >> addToQuery: aHornQuery [ 
 	aHornQuery qCon at: symbol put: sort
 ]
diff --git a/src/Refinements/HCstr.class.st b/src/Refinements/HCstr.class.st
index 87a54b324..be6b09d34 100644
--- a/src/Refinements/HCstr.class.st
+++ b/src/Refinements/HCstr.class.st
@@ -46,7 +46,7 @@ HCstr >> & anotherCstr [
 	^CstrAnd of: { self . anotherCstr }
 ]
 
-{ #category : #logic }
+{ #category : #construction }
 HCstr >> addToQuery: aNNFQuery [ 
 	aNNFQuery qCstr add: self
 ]
diff --git a/src/Refinements/HVar.class.st b/src/Refinements/HVar.class.st
index f68d26056..900e81e6b 100644
--- a/src/Refinements/HVar.class.st
+++ b/src/Refinements/HVar.class.st
@@ -34,7 +34,7 @@ HVar class >> name: aString argSorts: sorts [
 		yourself
 ]
 
-{ #category : #adding }
+{ #category : #construction }
 HVar >> addToQuery: q [ 
 	q addVar: self
 ]
diff --git a/src/Refinements/Qualifier.class.st b/src/Refinements/Qualifier.class.st
index 72111f26a..00633387e 100644
--- a/src/Refinements/Qualifier.class.st
+++ b/src/Refinements/Qualifier.class.st
@@ -24,7 +24,7 @@ Qualifier class >> true [
 	^self name: 'QTrue' params: #() body: nil
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #construction }
 Qualifier >> addToQuery: q [
 	q qualifiers add: self
 ]
diff --git a/src/Refinements/TC.class.st b/src/Refinements/TC.class.st
index 5fe9e8a9b..ddf132c06 100644
--- a/src/Refinements/TC.class.st
+++ b/src/Refinements/TC.class.st
@@ -17,7 +17,19 @@ instance Eq FTycon where
 	^symbol = rhs symbol
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #hotel }
+TC >> apply: ts [
+	| monoSymbol |
+	ts isEmpty ifTrue: [ ^self ].
+	monoSymbol :=
+		'(',
+		symbol,
+		(ts inject: '' into: [ :soFar :thisArgType | ' ', thisArgType unsafeName ]),
+		')'.
+	^TC symbol: monoSymbol
+]
+
+{ #category : #hotel }
 TC >> fTyconSort [
 	^FTC new: self
 ]
@@ -27,7 +39,7 @@ TC >> hash [
 	^symbol hash
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #hotel }
 TC >> isListTC [
 	^symbol isListConName
 ]
diff --git a/src/Refinements/Z3Sort.extension.st b/src/Refinements/Z3Sort.extension.st
index 87df290a1..e9ef207cb 100644
--- a/src/Refinements/Z3Sort.extension.st
+++ b/src/Refinements/Z3Sort.extension.st
@@ -94,6 +94,11 @@ Cf. Types/Sorts.hs
 
 ]
 
+{ #category : #'*Refinements' }
+Z3Sort >> monomorphicDeclIn: _ [ 
+	^self
+]
+
 { #category : #'*Refinements' }
 Z3Sort >> monomorphicSortName [
 	^self printString
diff --git a/src/SpriteLang-Tests/SpriteHornNegTest.class.st b/src/SpriteLang-Tests/SpriteHornNegTest.class.st
index 9c88b2da5..26ac6c763 100644
--- a/src/SpriteLang-Tests/SpriteHornNegTest.class.st
+++ b/src/SpriteLang-Tests/SpriteHornNegTest.class.st
@@ -489,3 +489,31 @@ SpriteHornNegTest >> testL6maxlist01 [
 
 '
 ]
+
+{ #category : #'tests-L6' }
+SpriteHornNegTest >> testL8uniqueVoidParam [
+	self proveNeg: '
+(data V 0 = [
+        | One {Cons0 : int}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]
+
+{ #category : #'tests-L6' }
+SpriteHornNegTest >> testL8uniqueVoidParamPoly [
+	self proveNeg: '
+(data V 1 = [
+        | One {Cons0 : @(0)}
+      ])
+ 
+(constraint
+    (forall ((a (V int)) (Bool true))
+      (forall ((b (V int)) (Bool true))
+          ((a === b)))))
+'
+]
diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
index bf961dc93..a2d417bcb 100644
--- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st
+++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
@@ -746,6 +746,34 @@ SpriteHornPosTest >> testL5cons00 [
 
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5cons00data [
+	self
+		provePos:
+			'
+(var $k3 ((`a) ((L `a)) (`a)))
+(var $k1 ((`a) (`a)))
+
+(constant len (func(1 , [(L @(0)); int])))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+  (forall ((x `a) (Bool true))
+   (forall ((t (L `a)) ((len value: t) === 0))
+     (and
+      (forall ((VV `a) (VV === x))
+       (($k3 VV t x)))
+      (forall ((VV0 `a)  ($k1 VV0 x))
+        (($k3 VV0 a x)))
+      (forall ((v (L `a)) ((len value: v) === (1 + (len value: t))))
+       ((((len value: v) === 1))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5foldRight00 [
 	self provePos: '
@@ -798,6 +826,35 @@ SpriteHornPosTest >> testL5head00 [
 '
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5head00data [
+	self provePos: '
+(var $k9 ((int) ((L int)) (int)))
+(var $k7 ((int) (int)))
+(var $k5 ((`a) ((L `a))))
+(var $k3 ((`a) ((L `a)) (`a)))
+(var $k1 ((`a) (`a)))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+ (and
+   (forall ((x `a)  (Bool true))
+     (forall ((t (L `a))  (Bool true))
+       (forall ((VV `a)  (VV === x)) (($k3 VV t x)))))
+   (forall ((z int)  (0 <= z))
+     (and
+       (forall ((v int) (and  (0 <= v) (v === z))) (($k7 v z)))
+       (forall ((l (L int))  (Bool true))
+        (and
+          (forall ((VV6 int)  ($k7 VV6 z)) (($k9 VV6 l z)))
+          (forall ((VV8 int)  ($k9 VV8 l z)) (((0 <= VV8))))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5head01 [
 	self provePos: '
@@ -1025,6 +1082,24 @@ SpriteHornPosTest >> testL5nil00 [
 
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5nil00data [
+	self provePos: '
+(constant len (func(1 , [(L @(0)); int])))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+   (forall ((x `a) (Bool true))
+    (forall ((t (L `a))  ((len value: t) === 0))
+      (forall ((v (L `a)) (and ((len value: v) === 0) (v === t))) ((((len value: v) === 0)))))))
+
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5olist00 [
 	self provePos: '
@@ -1603,3 +1678,18 @@ SpriteHornPosTest >> testL7sumAcc [
                    & (v < n))))))))))))))
 '
 ]
+
+{ #category : #'tests-L8' }
+SpriteHornPosTest >> testL8uniqueVoid [
+	"Cf. liquid-fixpoint/doodles/L8uniqueVoid.smt2 on branch experiment-z3datatypes"
+	self provePos: '
+(data V 0 = [
+        | Nil {}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]