diff --git a/src/Refinements/Z3BoolSort.extension.st b/src/Refinements/Z3BoolSort.extension.st
index a2b714638..2ddcdb022 100644
--- a/src/Refinements/Z3BoolSort.extension.st
+++ b/src/Refinements/Z3BoolSort.extension.st
@@ -5,11 +5,6 @@ Z3BoolSort >> containsFVar [
 	^false
 ]
 
-{ #category : #'*Refinements' }
-Z3BoolSort >> functionSort [
-	^nil
-]
-
 { #category : #'*Refinements' }
 Z3BoolSort >> isMono [
 	^true
diff --git a/src/Refinements/Z3DatatypeSort.extension.st b/src/Refinements/Z3DatatypeSort.extension.st
new file mode 100644
index 000000000..fe0a6515f
--- /dev/null
+++ b/src/Refinements/Z3DatatypeSort.extension.st
@@ -0,0 +1,6 @@
+Extension { #name : #Z3DatatypeSort }
+
+{ #category : #'*Refinements' }
+Z3DatatypeSort >> containsFVar [
+	^false
+]
diff --git a/src/Refinements/Z3IntSort.extension.st b/src/Refinements/Z3IntSort.extension.st
index cff937501..09a88a676 100644
--- a/src/Refinements/Z3IntSort.extension.st
+++ b/src/Refinements/Z3IntSort.extension.st
@@ -10,11 +10,6 @@ Z3IntSort >> containsFVar [
 	^false
 ]
 
-{ #category : #'*Refinements' }
-Z3IntSort >> functionSort [
-	^nil
-]
-
 { #category : #'*Refinements' }
 Z3IntSort >> isMono [
 	^true
diff --git a/src/Refinements/Z3Sort.extension.st b/src/Refinements/Z3Sort.extension.st
index e9ef207cb..bc72debde 100644
--- a/src/Refinements/Z3Sort.extension.st
+++ b/src/Refinements/Z3Sort.extension.st
@@ -32,6 +32,11 @@ Z3Sort >> falseRefinement [
 	^self | [ :x | Bool false ]
 ]
 
+{ #category : #'*Refinements' }
+Z3Sort >> functionSort [
+	^nil
+]
+
 { #category : #'*Refinements' }
 Z3Sort >> goFunctionSort: vs _: ss [ 
 	^{ vs reversed . ss reversed . self }
diff --git a/src/Refinements/Z3UninterpretedSort.extension.st b/src/Refinements/Z3UninterpretedSort.extension.st
index 46cae70c1..d086096bf 100644
--- a/src/Refinements/Z3UninterpretedSort.extension.st
+++ b/src/Refinements/Z3UninterpretedSort.extension.st
@@ -20,11 +20,6 @@ Z3UninterpretedSort >> containsFVar [
 	^true
 ]
 
-{ #category : #'*Refinements' }
-Z3UninterpretedSort >> functionSort [
-	^nil "functionSort $ FObj (symbol 'a') >> Nothing"
-]
-
 { #category : #'*Refinements' }
 Z3UninterpretedSort >> guest [
 	^PreSort hotel at: self unsafeName
diff --git a/src/SpriteLang/Data.class.st b/src/SpriteLang/Data.class.st
index a5b4e8d6a..fa11a5c27 100644
--- a/src/SpriteLang/Data.class.st
+++ b/src/SpriteLang/Data.class.st
@@ -32,6 +32,15 @@ Data class >> name: ident vars: idents rvars: rvars ctors: bindToRType_Assocs in
 		yourself
 ]
 
+{ #category : #checking }
+Data >> checkData: aΓContext [
+"
+checkData :: Env -> SrcData -> CG SrcCstr
+"
+	"BOGUS"
+	^CstrAnd of: #()
+]
+
 { #category : #accessing }
 Data >> ctors [
 	^ ctors
@@ -109,6 +118,22 @@ Data >> printOn: aStream [
 	
 ]
 
+{ #category : #reflect }
+Data >> reflectData [
+"
+---------------------------------------------------------------------------------
+reflectData :: SrcData -> F.DataDecl
+---------------------------------------------------------------------------------
+"
+	| tvM fCtors |
+	tvM := vars zip: (0 to: vars size - 1) with: [ :a :i | a -> (FVar new: i) ].
+	fCtors := ctors collectAssociations: [ :bind :s | s reflectCtor: bind tvSub: tvM ].
+	^DataDecl
+		ddTyCon: name symbolFTycon
+		ddVars: vars size
+		ddCtors: fCtors
+]
+
 { #category : #accessing }
 Data >> rvars [
 	^ rvars
diff --git a/src/SpriteLang/FunSig.class.st b/src/SpriteLang/FunSig.class.st
new file mode 100644
index 000000000..6044aa500
--- /dev/null
+++ b/src/SpriteLang/FunSig.class.st
@@ -0,0 +1,61 @@
+Class {
+	#name : #FunSig,
+	#superclass : #Object,
+	#instVars : [
+		'fsTVars',
+		'fsRVars',
+		'fsParams',
+		'fsOut'
+	],
+	#category : #SpriteLang
+}
+
+{ #category : #'instance creation' }
+FunSig class >> tVars: tVars rVars: rVars params: params out: out [
+	^self basicNew
+		fsTVars: tVars;
+		fsRVars: rVars;
+		fsParams: params;
+		fsOut: out;
+		yourself
+]
+
+{ #category : #accessing }
+FunSig >> fsOut [
+	^ fsOut
+]
+
+{ #category : #accessing }
+FunSig >> fsOut: anObject [
+	fsOut := anObject
+]
+
+{ #category : #accessing }
+FunSig >> fsParams [
+	^ fsParams
+]
+
+{ #category : #accessing }
+FunSig >> fsParams: anObject [
+	fsParams := anObject
+]
+
+{ #category : #accessing }
+FunSig >> fsRVars [
+	^ fsRVars
+]
+
+{ #category : #accessing }
+FunSig >> fsRVars: anObject [
+	fsRVars := anObject
+]
+
+{ #category : #accessing }
+FunSig >> fsTVars [
+	^ fsTVars
+]
+
+{ #category : #accessing }
+FunSig >> fsTVars: anObject [
+	fsTVars := anObject
+]
diff --git a/src/SpriteLang/Prog.class.st b/src/SpriteLang/Prog.class.st
index c2368a9d8..c8a793431 100644
--- a/src/SpriteLang/Prog.class.st
+++ b/src/SpriteLang/Prog.class.st
@@ -93,7 +93,7 @@ Prog >> solve [
 
 { #category : #verification }
 Prog >> vcgen [
-	| expr′ env eL ps pqs c_cgi c cgi rfls syms c′ query |
+	| expr′ env eL ps pqs cI c_cgi c cgi rfls syms c′ decs |
 	expr′ := expr uniq2.
 	env := ΓContext empEnv: meas typs: data.
 	eL := expr′ elaborate: env.
@@ -103,16 +103,18 @@ Prog >> vcgen [
 		hcon symbol -> hcon sort
 	].
 	pqs := #(1 2 3) collect: [ :j | Qualifier pappQual: j ].
+	cI := [ CstrAnd of: (data collect: [ :t | t checkData: env ]) ] runCG key.
 	c_cgi := [ eL check: env rtype: TInt instance bTrue ] runCG.
 	c := c_cgi key. cgi := c_cgi value.
 	rfls := cgi cgiConsts.
 	syms := Dictionary newFromAssociations: ps, meas, rfls.
 	c′ := c strengthenInv: env.
+	decs := data collect: #reflectData.
 	^HornQuery
 		mkQuery_qs: quals, pqs
 		ks: cgi cgiKVars
-		cstr: "cI &" c′
+		cstr: cI & c′
 		syms: syms
 		defs: cgi cgiDefs
-		ddecls: #()
+		ddecls: decs
 ]
diff --git a/src/SpriteLang/RType.class.st b/src/SpriteLang/RType.class.st
index abe3c41ba..96462182c 100644
--- a/src/SpriteLang/RType.class.st
+++ b/src/SpriteLang/RType.class.st
@@ -168,6 +168,20 @@ fresh :: F.SrcSpan -> Env -> RType -> CG RType
 	self subclassResponsibility
 ]
 
+{ #category : #reflect }
+RType >> funSig [
+"
+funSig :: RType -> FunSig
+"
+	| as_rs_t′ as rs t′ xts_ot xts ot |
+	as_rs_t′ := self bkAlls.
+	as := as_rs_t′ first. rs := as_rs_t′ second. t′ := as_rs_t′ third.
+	xts_ot := t′ bkFun.
+	xts := xts_ot key.
+	ot := xts_ot value.
+	^FunSig tVars: as rVars: rs params: xts out: ot
+]
+
 { #category : #'as yet unclassified' }
 RType >> generalize [
 	"Normalize types by generalizing tyvars, refactoring ref-var applications."
@@ -409,6 +423,25 @@ reflect :: Ident -> SrcExpr -> RType -> CG RType
 	^self reflectTy: f v: v expr: e
 ]
 
+{ #category : #reflect }
+RType >> reflectCtor: bind tvSub: tvSub [
+"
+reflectCtor :: TvSub -> (SrcBind, RType) -> F.DataCtor
+Cf. Reflect.hs
+NB: Here TvSub is 'type TvSub = [(Ident, F.Sort)]', not the other one!
+"
+	| fldTs fFields |
+	fldTs := self funSig fsParams collect: #value.
+	fFields := fldTs zip: (0 to: fldTs size - 1) with: [ :t :i |
+		| fldName fldSort |
+		fldName := bind id selDataCon: i.
+		fldSort := t rtypeSort sortSubst: (Dictionary newFromAssociations: tvSub).
+		DataField dfName: fldName dfSort: fldSort ].
+	^DataCtor
+		dcName: bind id
+		dcFields: fFields
+]
+
 { #category : #reflect }
 RType >> reflectTy: f v: v expr: e [
 "
diff --git a/src/SpriteLang/String.extension.st b/src/SpriteLang/String.extension.st
index b8d782e41..92f034ca6 100644
--- a/src/SpriteLang/String.extension.st
+++ b/src/SpriteLang/String.extension.st
@@ -39,6 +39,14 @@ rVar :: F.Symbol -> RType
 	^(TVar symbol: self) bTrue
 ]
 
+{ #category : #'*SpriteLang' }
+String >> selDataCon: i [
+"
+selDataCon :: DaCon -> Int -> F.Symbol
+"
+	^self intSymbol: i
+]
+
 { #category : #'*SpriteLang' }
 String >> unifyX: anotherString [ 
 	^self
diff --git a/src/SpriteLang/TCon.class.st b/src/SpriteLang/TCon.class.st
index fde4d6d5b..48ff51943 100644
--- a/src/SpriteLang/TCon.class.st
+++ b/src/SpriteLang/TCon.class.st
@@ -132,6 +132,11 @@ TCon >> reft [
 	^r
 ]
 
+{ #category : #'as yet unclassified' }
+TCon >> rtypeSort [
+	^c symbolFTycon fAppTC: (ts collect: #rtypeSort)
+]
+
 { #category : #'synthesis constraints' }
 TCon >> singleton: x [
 	^TCon