type.d

// Written in the D programming language
// License: http://www.boost.org/LICENSE_1_0.txt, Boost License 1.0
module ast.type;
import astopt;
import std.format: format;

enum CaptureAnnotation{
	none,
	const_,
	moved,
	once,
	spent,
}

static if(language==silq){
	enum Annotation{
		none,
		mfree,
		qfree,
	}
	enum deterministic=Annotation.mfree;
	enum pure_=Annotation.qfree;
}else static if(language==psi){
	enum Annotation{
		none,
		pure_,
		mfree=pure_, // (for code shared with Silq)
		qfree=pure_, // (for code shared with Silq)
	}
	enum deterministic=Annotation.pure_;
	enum pure_=Annotation.pure_;
}

import std.array, std.algorithm, std.conv;
import std.functional, std.range;
import ast.expression, ast.declaration, util;
import ast.modules: isInPrelude;
import ast.scope_: Scope, TypeTransition;
import util: MapX, MapSX;

// The type constructors below share one instance per distinct argument list.
// std.functional.memoize would keep every instance for the life of the
// process, which a long-running host cannot afford: each check builds fresh
// types (a 𝔹^n for each new n), so each check would leave its syntax tree
// reachable from the cache. These caches can be dropped between checks with
// clearTypeCaches. A one-shot compile never does, and behaves as before.
private void function()[] typeCacheClearers;

void clearTypeCaches(){
	foreach(clear;typeCacheClearers) clear();
}

private template memoize(alias fun){
	import std.traits: Parameters, ReturnType;
	import std.typecons: Tuple;
	alias Args=Tuple!(Parameters!fun);
	ReturnType!fun[Args] cache;
	bool registered=false;
	ReturnType!fun memoize(Parameters!fun args){
		if(!registered){
			registered=true;
			typeCacheClearers~=function(){ cache=null; };
		}
		auto key=Args(args);
		if(auto r=key in cache) return *r;
		auto r=fun(args);
		cache[key]=r;
		return r;
	}
}

enum NumericType{
	none,
	Bool,
	ℕt,
	ℤt,
	ℚt,
	ℝ,
	ℂ,
}

NumericType isNumericTy(Expression t){
	if(!t) return NumericType.none;
	t=unfoldTypeVariable(t);
	auto ty = cast(NumericTy)t;
	if(!ty) return NumericType.none;
	return ty.nty;
}

struct FixedIntTy {
	Expression bits;
	bool isSigned, isClassical;

	bool opCast(T: bool)() const pure @safe nothrow {
		return !!bits;
	}
}

FixedIntTy isFixedIntTy(Expression e){
	assert(e&&e.isSemEvaluated());
	e=unfoldTypeVariable(e);
	auto ce=cast(CallExp)e;
	if(!ce || !ce.isSquare) return FixedIntTy();
	auto bits=ce.arg;
	bool isClassical=ce.isClassical_;

	auto id=cast(Identifier)ce.e;
	if(!id||!id.meaning||!isInPrelude(id.meaning)) return FixedIntTy();

	bool isSigned;
	switch(id.name){
		case "int":
			isSigned=true;
			break;
		case "uint":
			isSigned=false;
			break;
		default:
			return FixedIntTy();
	}
	return FixedIntTy(bits, isSigned, isClassical);
}

bool isInt(Expression e){
	if(auto ty=isFixedIntTy(e)) return ty.isSigned;
	else return false;
}
bool isUint(Expression e){
	if(auto ty=isFixedIntTy(e)) return !ty.isSigned;
	else return false;
}

struct ℤmodTy{
	Expression N;
	bool isStar,isClassical;
	bool opCast(T:bool)(){
		return !!N;
	}
}

ℤmodTy isℤmodTy(Expression e){
	assert(e&&e.isSemEvaluated());
	e=unfoldTypeVariable(e);
	auto ce=cast(CallExp)e;
	if(!ce||!ce.isSquare) return ℤmodTy();
	auto id=cast(Identifier)ce.e;
	if(!id||!id.meaning||!isInPrelude(id.meaning)) return ℤmodTy();
	bool isStar=id.name=="ℤstar";
	if(!isStar&&id.name!="ℤmod") return ℤmodTy();
	auto N=ce.arg;
	auto isClassical=ce.isClassical_;
	return ℤmodTy(N,isStar,isClassical);
}


string preludeNumericTypeName(Expression e){
	auto ce=cast(CallExp)e;
	if(!ce || !ce.isSquare) return null;
	auto id=cast(Identifier)ce.e;
	if(!id||!id.meaning||!isInPrelude(id.meaning)) return null;
	return id.name;
}

bool isFloat(Expression e){ return preludeNumericTypeName(e)=="float"; }
bool isRat(Expression e){ return preludeNumericTypeName(e)=="rat"; }

bool isSubtype(Expression lhs,Expression rhs,EqualityContext* ctx=null){
	if(isSubtypeShallow(lhs,rhs,ctx)) return true;
	static if(language==silq) if(lhs&&rhs){ // (through the values of type variables, see `unfoldTypeVariables`)
		auto ul=unfoldTypeVariables(lhs),ur=unfoldTypeVariables(rhs);
		if(ul !is lhs||ur !is rhs) return isSubtypeShallow(ul,ur,ctx);
	}
	return false;
}
private bool isSubtypeShallow(Expression lhs,Expression rhs,EqualityContext* ctx){
	if(!lhs||!rhs) return false;
	assert(lhs.isSemEvaluated());
	assert(rhs.isSemEvaluated());
	if(lhs is rhs) return true;
	if(lhs.isClassical()&&!rhs.isClassical()&&!isEmpty(lhs)) { // (empty types are classical, but may have quantum components)
		rhs = rhs.getClassical();
		if(!rhs) return false;
		if(lhs is rhs) return true;
	} else if(!lhs.isClassical()&&rhs.isClassical()) {
		return false;
	}
	return lhs.isSubtypeImpl(rhs,ctx);
}

Expression combineTypes(Expression lhs,Expression rhs,bool meet,bool allowQNumeric=false){ // TODO: more general solution // TODO: ⊤/⊥?
	if(!lhs||!rhs) return null;
	if(isEmpty(lhs)) return meet?lhs:rhs;
	if(isEmpty(rhs)) return meet?rhs:lhs;
	if(lhs == rhs) return lhs;
	auto l=lhs.eval(), r=rhs.eval();
	if(isEmpty(lhs)) return meet?lhs:rhs;
	if(isEmpty(rhs)) return meet?rhs:lhs;
	auto result = l.combineTypesImpl(r,meet);
	static if(language==silq) if(!result){ // (through the values of type variables, see `unfoldTypeVariables`)
		if(isSubtype(l,r)) return meet?lhs:rhs;
		if(isSubtype(r,l)) return meet?rhs:lhs;
		auto ul=unfoldTypeVariables(l),ur=unfoldTypeVariables(r);
		if(ul !is l||ur !is r) result=ul.combineTypesImpl(ur,meet);
	}
	if(!allowQNumeric && isQNumeric(result)) return null;
	return result;
}

Expression joinTypes(Expression lhs,Expression rhs){
	return combineTypes(lhs,rhs,false);
}
Expression meetTypes(Expression lhs,Expression rhs){
	return combineTypes(lhs,rhs,true);
}

abstract class Type: Expression{
	override @property string kind(){ return "type"; }
	override string toString(){ return "T"; }
	override Annotation getAnnotation(){ return pure_; }
}

class NumericTy: Type{
	private NumericType nty;
	static if(language==silq) {
		private bool classical;
		private this(NumericType nty, bool classical){
			assert(nty);
			assert(!theNumeric[nty][classical]);
			this.nty = nty;
			this.classical = classical;
			this.type = classical ? ctypeTy() : nty == NumericType.Bool ? qtypeTy() : qnumericTy();
			setSemEvaluated();
		}
	} else {
		private enum classical=true;
		private this(NumericType nty) {
			assert(!theNumeric[nty]);
			this.nty = nty;
			this.type = typeTy();
			setSemEvaluated();
		}
	}
	override NumericTy getClassical(){
		if(this.classical) return this;
		return numericTy(this.nty, true);
	}
	override NumericTy getQuantum(){
		if(!this.classical) return this;
		return numericTy(this.nty, false);
	}
	override Expression combineTypesImpl(Expression r, bool meet){
		auto ty = cast(NumericTy)r;
		if(!ty) return null;
		if(meet) return numericTy(min(nty, ty.nty), classical || ty.classical);
		return numericTy(max(nty, ty.nty), classical && ty.classical);
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		auto ty = cast(NumericTy)r;
		if(!ty) return false;
		assert(ty !is this);
		return nty <= ty.nty && classical >= ty.classical;
	}
	override NumericTy copyImpl(CopyArgs args){
		return this;
	}
	override string toString(){
		size_t i = 1;
		static if(language==silq) {
			i = !classical;
		}
		final switch(nty) {
			case NumericType.none: assert(0);
			case NumericType.Bool: return "!𝔹"[i..$];
			case NumericType.ℕt: return "!ℕ"[i..$];
			case NumericType.ℤt: return "!ℤ"[i..$];
			case NumericType.ℚt: return "!ℚ"[i..$];
			case NumericType.ℝ: return "!ℝ"[i..$];
			case NumericType.ℂ: return "!ℂ"[i..$];
		}
	}
	override bool isConstant(){ return true; }
	override bool isTotal(){ return true; }
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) dg){
		return 0;
	}
}
static if(language==silq) private NumericTy[2][7] theNumeric;
else private NumericTy[7] theNumeric;

NumericTy Bool(bool classical=true){
	return numericTy(NumericType.Bool, classical);
}

NumericTy ℕt(bool classical=true){
	return numericTy(NumericType.ℕt, classical);
}

NumericTy ℤt(bool classical=true){
	return numericTy(NumericType.ℤt, classical);
}

NumericTy ℚt(bool classical=true){
	return numericTy(NumericType.ℚt, classical);
}

NumericTy ℝ(bool classical=true){
	return numericTy(NumericType.ℝ, classical);
}

NumericTy ℂ(bool classical=true){
	return numericTy(NumericType.ℂ, classical);
}

NumericTy numericTy(NumericType which, bool classical){
	if(!which) return null;
	static if(language==silq){
		return theNumeric[which][classical] ? theNumeric[which][classical] : (theNumeric[which][classical] = new NumericTy(which, classical));
	} else {
		return theNumeric[which] ? theNumeric[which] : (theNumeric[which] = new NumericTy(which));
	}
}


class AggregateTy: Type{
	DatDecl decl;
	static if(language==silq){
		bool classical;
		private AggregateTy classicalTy;
		private AggregateTy quantumTy;
	}else enum classical=true;
	this(DatDecl decl,bool classical,AggregateTy classicalTy=null,AggregateTy quantumTy=null){
		if(!classical) assert(decl.isQuantum);
		this.decl=decl;
		static if(language==silq){
			this.classical=classical;
			if(classical) this.classicalTy=this;
			else this.classicalTy=classicalTy?classicalTy:New!AggregateTy(decl,true,null,decl.isQuantum?this:null);
			if(decl.isQuantum){
				if(!classical) this.quantumTy=this;
				else this.quantumTy=quantumTy?quantumTy:New!AggregateTy(decl,false,this,null);
			}
		}
		this.type=typeTy(); // TODO
		setSemEvaluated();
	}
	override AggregateTy copyImpl(CopyArgs args){
		return this;
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		if(auto r=cast(AggregateTy)rhs)
			return decl is r.decl && classical==r.classical;
		return false;
	}
	override string toString(){
		return decl&&decl.name?decl.name.name:"<anonymous aggregate>";
	}
	override bool isConstant(){ return true; }
	override bool isTotal(){ return true; }
	override AggregateTy getClassical(){
		static if(language==silq) return classicalTy;
		else return this;
	}
	override AggregateTy getQuantum(){
		static if(language==silq) return quantumTy;
		else return this;
	}

	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) e){
		return 0;
	}
}

class ContextTy: Type{
	static if(language==silq) private bool classical;
	else private enum classical=true;
	private this(bool classical){
		static if(language==silq) this.classical=classical;
		this.type = classical ? ctypeTy() : typeTy();
		setSemEvaluated();
	}
	override ContextTy copyImpl(CopyArgs args){
		return this;
	}
	override bool isConstant(){ return true; }
	override bool isTotal(){ return true; }
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		auto r=cast(ContextTy)rhs;
		return r&&r.classical==classical;
	}
	override string toString(){
		static if(language==silq) return (classical?"!":"")~"`Ctx";
		else return "`Ctx";
	}
	override ContextTy getClassical(){
		return contextTy(true);
	}
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) e){
		return 0;
	}
}
static if(language==silq) private ContextTy[2] theContextTy;
else private ContextTy theContextTy;
ContextTy contextTy(bool classical=true){
	static if(language==silq) return theContextTy[classical]?theContextTy[classical]:(theContextTy[classical]=new ContextTy(classical));
	else return theContextTy?theContextTy:(theContextTy=new ContextTy(true));
}


class BottomTy: Type{
	this(){
		type = etypeTy;
		setSemEvaluated();
	}
	override BottomTy copyImpl(CopyArgs args){
		return this;
	}
	override string toString(){
		return "⊥";
	}
	override bool isConstant(){ return true; }
	override bool isTotal(){ return true; }
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		return !!cast(BottomTy)rhs;
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		return true;
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		return meet?this:r;
	}
	override BottomTy getClassical(){
		return this;
	}
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) e){
		return 0;
	}
}
private BottomTy theBottomTy;
BottomTy bottom(){
	return theBottomTy?theBottomTy:(theBottomTy=new BottomTy());
}


class ClassicalTy: Expression{
	Expression inner;
	this(Expression inner){
		this.inner = inner;
	}
	override string toString(){
		return "!" ~ inner.toString();
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		auto r=cast(ClassicalTy)rhs;
		if(!r) return false;
		return isEqual(inner,r.inner,&ctx);
	}
	override ClassicalTy copyImpl(CopyArgs args){
		return new ClassicalTy(inner.copy(args));
	}
	override int componentsImpl(scope int delegate(Expression) dg){
		return dg(inner);
	}
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		return inner.freeVarsImpl(dg);
	}
	override Expression substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		return new ClassicalTy(inner.substitute(subst,tt));
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		assert(false);
	}
	override Annotation getAnnotation(){
		return pure_;
	}
	override Expression evalImpl(){
		return inner.eval().getClassical();
	}
}


interface ITupleTy{
	@property size_t length();
	Expression opIndex(size_t i);
	Expression opSlice(size_t l,size_t r);
}

class TupleTy: Type,ITupleTy{
	Expression[] types;
	override ITupleTy isTupleTy(){ return this; }
	@property size_t length(){ return types.length; }
	Expression opIndex(size_t i){ return types[i]; }
	Expression opSlice(size_t l,size_t r){ return tupleTy(types[l..r]); }
	this(Expression[] types)in{
		assert(types.all!());
	}do{
		this.types=types;
	}
	override TupleTy copyImpl(CopyArgs args){
		return new TupleTy(types.map!(ty => ty.copy(args)).array);
	}
	override string toString(){
		if(!types.length) return "𝟙";
		if(types.length==1) return "("~types[0].toString()~")¹";
		string addp(Expression a){
			if(cast(FunTy)a) return "("~a.toString()~")";
			return a.toString();
		}
		return types.map!(a=>a.isTupleTy()&&a!=unit?"("~a.toString()~")":addp(a)).join(" × ");
	}
	override bool isConstant(){ return types.all!(ty=>ty.isConstant()); }
	override bool isTotal(){ return types.all!(ty=>ty.isTotal()); }
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		foreach(t;types)
			if(auto r=t.freeVarsImpl(dg))
				return r;
		return 0;
	}
	override Type substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		auto ntypes=types.dup;
		foreach(ref t;ntypes) t=t.substitute(subst,tt);
		if(iota(types.length).all!(i => ntypes[i] is types[i])) return this;
		return tupleTy(ntypes);
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		auto tt=rhs.isTupleTy();
		if(!tt||types.length!=tt.length) return false;
		return all!(i=>types[i].unify(tt[i],subst,meet))(iota(types.length));

	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		if(auto r=cast(TupleTy)rhs){
			if(types.length!=r.types.length) return false;
			return all!(i=>isEqual(types[i],r.types[i],&ctx))(iota(types.length));
		}
		return false;
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		auto ltup=this,rtup=r.isTupleTy();
		if(rtup&&ltup.types.length==rtup.length)
			return all!(i=>isSubtype(ltup.types[i],rtup[i],ctx))(iota(ltup.types.length));
		auto rarr=cast(ArrayTy)r;
		if(rarr) return all!(i=>isSubtype(ltup.types[i],rarr.next,ctx))(iota(ltup.types.length));
		static if(language==silq) if(auto rvec=cast(VectorTy)r) if(!rtup&&isEqual(LiteralExp.makeInteger(ltup.types.length),rvec.num,ctx)) // (e.g., `!𝔹^n` after `n:=3`)
			return all!(i=>isSubtype(ltup.types[i],rvec.next,ctx))(iota(ltup.types.length));
		return false;
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		auto ltup=this,rtup=r.isTupleTy();
		if(rtup&&ltup.types.length==rtup.length){
			auto rtypes=zip(ltup.types,iota(rtup.length).map!(i=>rtup[i])).map!((t)=>combineTypes(t.expand,meet)).array;
			if(all!(x=>x !is null)(rtypes)) return tupleTy(rtypes);
		}
		auto rarr=cast(ArrayTy)r;
		if(!rarr&&!meet){
			if(auto rvec=cast(VectorTy)r)
				rarr=arrayTy(rvec.next);
			if(rtup&&!meet){
				if(auto next=chain(ltup.types,iota(rtup.length).map!(i=>rtup[i])).fold!((a,b)=>combineTypes(a,b,meet))(cast(Expression)bottom))
					rarr=arrayTy(next);
			}
		}
		if(rarr){
			if(meet){
				auto rtypes=zip(ltup.types,iota(length).map!(i=>rarr.next)).map!((t)=>combineTypes(t.expand,meet)).array;
				if(all!(x=>x !is null)(rtypes)) return tupleTy(rtypes);
			}else{
				auto rtype=ltup.types.fold!((a,b)=>combineTypes(a,b,meet))(rarr.next);
				if(rtype) return arrayTy(rtype);
			}
		}
		return null;
	}
	override Expression getClassical(){
		auto ntypes=types.map!(x=>x.getClassical()).array;
		if(all!(x=>x !is null)(ntypes)) return tupleTy(ntypes);
		return null;
	}
	override Expression getQuantum(){
		auto ntypes=types.map!(x=>x.getQuantum()).array;
		if(all!(x=>x !is null)(ntypes)) return tupleTy(ntypes);
		return null;
	}
	override bool mayBeClassical(){ return types.all!(x=>x.mayBeClassical()); }
	override bool mayBeQuantum(){ return types.all!(x=>x.mayBeQuantum()); }
	override int componentsImpl(scope int delegate(Expression) dg){
		foreach(x;types) if(auto r=dg(x)) return r;
		return 0;
	}
	override Expression evalImpl(){
		assert(isTypeTy(type) || isQNumericTy(type));
		auto ntypes=types.map!(t=>t.eval()).array;
		auto r=tupleTy(ntypes); // (e.g., a product type of the source, `𝔹×𝔹` is `𝔹^2`)
		if(cast(TupleTy)r&&iota(types.length).all!(i => ntypes[i] is types[i])) return this;
		return r;
	}
}

Type unit(){ return tupleTy([]); }

Type tupleTy(Expression[] types)in{
	assert(types.all!(e=>isType(e)||isQNumeric(e)));
	assert(types.all!(e=>e.isSemEvaluated()));
}do{
	import ast.lexer: Token,Tok;
	if(types.length&&types.all!(x=>x==types[0])){
		return vectorTy(types[0], types.length);
	}
	return memoize!((Expression[] types){
		auto r = new TupleTy(types);
		r.type = typeOfTupleTy(r.types);
		r.setSemEvaluated();
		return r;
	})(types);
}

size_t numComponents(Expression t){
	if(auto tpl=t.isTupleTy())
		return tpl.length;
	return 1;
}

class ArrayTy: Type{
	Expression next;
	this(Expression next)in{
		assert(next);
	}do{
		this.next=next;
	}
	override ArrayTy copyImpl(CopyArgs args){
		return new ArrayTy(next.copy(args));
	}
	override string toString(){
		bool p=cast(FunTy)next||next.isTupleTy()&&next!=unit;
		return p?"("~next.toString()~")[]":next.toString()~"[]";
	}
	override bool isConstant(){ return next.isConstant(); }
	override bool isTotal(){ return next.isTotal(); }
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		return next.freeVarsImpl(dg);
	}
	override ArrayTy substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		return arrayTy(next.substitute(subst,tt));
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		if(auto vt=cast(VectorTy)rhs)
			return next.unify(vt.next,subst,meet);
		if(auto tt=cast(TupleTy)rhs)
			return tt.types.all!(ty=>next.unify(ty,subst,meet));
		if(auto at=cast(ArrayTy)rhs)
			return next.unify(at.next,subst,meet);
		return false;
	}
	override ArrayTy evalImpl(){
		assert(isTypeTy(type) || isQNumericTy(type));
		return arrayTy(next.eval());
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		if(auto r=cast(ArrayTy)rhs)
			return isEqual(next,r.next,&ctx);
		return false;
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		auto larr=this,rarr=cast(ArrayTy)r;
		if(!rarr) return false;
		return isSubtype(larr.next,rarr.next,ctx);
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		auto larr=this,rarr=cast(ArrayTy)r;
		if(rarr){
			auto combinedNext=combineTypes(larr.next,rarr.next,meet);
			if(combinedNext) return arrayTy(combinedNext);
		}
		if(auto rvec=cast(VectorTy)r){
			auto nnext=combineTypes(next,rvec.next,meet);
			if(nnext){
				if(meet) return vectorTy(nnext,rvec.num);
				else return arrayTy(nnext);
			}
			auto len=rvec.num.asIntegerConstant(true);
			if(!len||len.get()!=0) return null;
		}
		if(auto rtup=r.isTupleTy()){
			if(meet){
				auto ntypes=iota(rtup.length).map!(i=>combineTypes(next,rtup[i],meet)).array;
				if(all!(x=>x !is null)(ntypes)) return tupleTy(ntypes);
			}else{
				auto rtype=iota(rtup.length).map!(i=>rtup[i]).fold!((a,b)=>a?combineTypes(a,b,meet):null)(next);
				if(rtype) return arrayTy(rtype);
			}
		}
		return null;
	}
	override Expression getClassical(){
		auto nnext=next.getClassical();
		if(!nnext) return null;
		return arrayTy(nnext);
	}
	override Expression getQuantum(){
		return null; // length is classical
	}
	override bool mayBeClassical(){ return next.mayBeClassical(); }
	override bool mayBeQuantum(){ return false; } // TODO: ok?
	override int componentsImpl(scope int delegate(Expression) dg){
		return dg(next);
	}
}

ArrayTy arrayTy(Expression next)in{
	assert(isType(next)||isQNumeric(next));
	assert(next.isSemEvaluated());
}do{
	return memoize!((Expression next){
		auto r = new ArrayTy(next);
		r.type = typeOfArrayTy(next);
		r.setSemEvaluated();
		return r;
	})(next);
}

class VectorTy: Type, ITupleTy{
	Expression next,num;
	this(Expression next,Expression num)in{
		assert(next);
		assert(num);
	}do{
		this.next=next;
		this.num=num;
	}
	override ITupleTy isTupleTy(){
		if(auto len=num.asIntegerConstant())
			if(len.get()<=size_t.max) return this;
		return null;
	}
	override VectorTy copyImpl(CopyArgs args){
		return new VectorTy(next.copy(args), num.copy(args));
	}
	@property size_t length(){
		auto iconst=num.asIntegerConstant();
		assert(!!iconst);
		return iconst.get().to!size_t(); // TODO: avoid crash if length is too big
	}
	Expression opIndex(size_t i){ return next; }
	Expression opSlice(size_t l,size_t r){
		assert(0<=l&&l<=r&&r<=length);
		auto len=LiteralExp.makeInteger(r-l);
		return vectorTy(next,len);
	}
	override string toString(){
		import ast.parser: rbp;
		import ast.lexer: Tok;
		bool p=cast(FunTy)next||next.isTupleTy&&next!=unit;
		return (p?"("~next.toString()~")^":next.toString()~"^")~num.toStringImpl(rbp!(Tok!"^"),Expression.prNone);
	}
	override bool isConstant(){ return next.isConstant() && num.isConstant(); }
	override bool isTotal(){ return next.isTotal() && num.isTotal(); }
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		if(auto r=next.freeVarsImpl(dg)) return r;
		return num.freeVarsImpl(dg);
	}
	override Expression substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		auto nnext=next.substitute(subst,tt),nnum=num.substitute(subst,tt);
		if(!nnum.type||!isSubtype(nnum.type,ℕt(true))) return arrayTy(nnext);
		return vectorTy(nnext,nnum);
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		if(auto tt=cast(TupleTy)rhs)
			return tt.types.all!(ty=>next.unify(ty,subst,meet)) && num.unify(LiteralExp.makeInteger(tt.length),subst,meet);
		if(auto vt=cast(VectorTy)rhs){
			auto r=next.unify(vt.next,subst,meet);
			if(auto nlit=num.asIntegerConstant())
				if(nlit.get()==0&&num==vt.num) return true;
			return r && num.unify(vt.num,subst,meet);
		}
		return false;
	}
	override VectorTy evalImpl(){
		assert(isTypeTy(type) || isQNumericTy(type));
		return vectorTy(next.eval(),num.eval());
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		if(auto r=cast(VectorTy)rhs)
			return isEqual(next,r.next,&ctx)&&isEqual(num,r.num,&ctx);
		return false;
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		if(auto rarr=cast(ArrayTy)r){
			if(auto nlit=num.asIntegerConstant())
				if(nlit.get()==0) return true; // (as for an empty tuple, e.g., when the array type was made classical)
			return isSubtype(next,rarr.next,ctx);
		}
		auto lvec=this,rvec=cast(VectorTy)r;
		if(rvec){
			if(!isEqual(num,rvec.num,ctx)) return false;
			if(auto nlit=num.asIntegerConstant())
				if(nlit.get()==0) return true;
			return isSubtype(lvec.next,rvec.next,ctx);
		}
		auto ltup=this.isTupleTy(),rtup=r.isTupleTy();
		if(ltup&&rtup&&ltup.length==rtup.length)
			return all!(i=>isSubtype(ltup[i],rtup[i]))(iota(ltup.length));
		static if(language==silq) if(!ltup&&rtup&&isEqual(num,LiteralExp.makeInteger(rtup.length),ctx)) // (e.g., `!𝔹^n` after `n:=3`)
			return all!(i=>isSubtype(next,rtup[i],ctx))(iota(rtup.length));
		return false;
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		if(auto rarr=cast(ArrayTy)r){
			auto nnext=combineTypes(next,rarr.next,meet);
			if(nnext){
				if(meet) return vectorTy(nnext,num);
				else return arrayTy(nnext);
			}
		}
		auto lvec=this,rvec=cast(VectorTy)r;
		if(rvec){
			auto nnext=combineTypes(lvec.next,rvec.next,meet);
			if(!nnext) return null;
			if(num==rvec.num){
				return vectorTy(nnext,num);
			}else if(!meet){
				return arrayTy(nnext);
			}else return null;
		}
		auto ltup=this.isTupleTy(),rtup=r.isTupleTy();
		if(rtup){
			bool equal=false;
			if(ltup) equal=ltup.length==rtup.length;
			else equal=num==LiteralExp.makeInteger(rtup.length);
			if(equal){
				auto rtypes=iota(rtup.length).map!(i=>combineTypes(next,rtup[i],meet)).array;
				if(all!(x=>x !is null)(rtypes)) return tupleTy(rtypes);
			}else if(!meet){
				auto nnext=iota(rtup.length).map!(i=>rtup[i]).fold!((a,b)=>combineTypes(a,b,meet))(next);
				if(nnext) return arrayTy(nnext);
			}else return null;
		}
		return null;
	}
	override Expression getClassical(){
		auto nnext=next.getClassical();
		if(!nnext) return null;
		return vectorTy(nnext,num);
	}
	override Expression getQuantum(){
		auto nnext=next.getQuantum();
		if(!nnext){
			if(isZero(num)) return unit;
			return null;
		}
		return vectorTy(nnext,num);
	}
	override bool mayBeClassical(){ return next.mayBeClassical(); }
	override bool mayBeQuantum(){ return next.mayBeQuantum(); }
	override int componentsImpl(scope int delegate(Expression) dg){
		if(auto r=dg(next)) return r;
		return dg(num);
	}
}

VectorTy vectorTy(Expression next,Expression num)in{
	assert(isType(next)||isQNumeric(next));
	assert(next.isSemEvaluated(), format("unevaluated vector item type %s", next));
	assert(num&&isSubtype(num.type,ℕt(true)));
	assert(num.isSemEvaluated(), format("unevaluated vector length %s", num));
}do{
	return memoize!((Expression next,Expression num){
		auto r = new VectorTy(next,num);
		r.type = typeOfVectorTy(next, num);
		r.setSemEvaluated();
		return r;
	})(next,num);
}
VectorTy vectorTy(Expression next, size_t num){
	return vectorTy(next, LiteralExp.makeInteger(num));
}

static Expression elementType(Expression ty){
	if(auto at=cast(ArrayTy)ty) return at.next;
	if(auto vt=cast(VectorTy)ty) return vt.next;
	return null;
}

class StringTy: Type{
	static if(language==silq) bool classical;
	else enum classical=true;
	private this(bool classical){
		this.type=typeOfStringTy(classical);
		setSemEvaluated();
	}
	override StringTy copyImpl(CopyArgs args){
		return this;
	}
	override string toString(){
		static if(language==silq) return classical?"!string":"string";
		else return "string";
	}
	override bool isConstant(){ return true; }
	override bool isTotal(){ return true; }
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) dg){
		return 0;
	}
}

StringTy stringTy(bool classical=true){
	static if(language==silq) return memoize!((bool classical)=>new StringTy(classical))(classical);
	else{
		static StringTy theStringTy;
		return theStringTy?theStringTy:(theStringTy=new StringTy(true));
	}
}

string captureAnnotationToString(CaptureAnnotation captureAnnotation){
	return captureAnnotation?captureAnnotation==CaptureAnnotation.const_?"const":text(captureAnnotation):"";
}

bool captureAnnotationSubtype(CaptureAnnotation captureAnnotation1,CaptureAnnotation captureAnnotation2){
	if(captureAnnotation1==captureAnnotation2) return true;
	if(!captureAnnotation1) return true;
	if(!captureAnnotation2) return false;
	if(captureAnnotation1==CaptureAnnotation.const_||captureAnnotation1==CaptureAnnotation.moved)
		if(captureAnnotation2==CaptureAnnotation.once)
			return true;
	if(captureAnnotation1==CaptureAnnotation.const_&&captureAnnotation2==CaptureAnnotation.spent)
		return true;
	return false;
}
bool captureAnnotationCombinable(CaptureAnnotation captureAnnotation1,CaptureAnnotation captureAnnotation2,bool meet){
	if(captureAnnotation1==captureAnnotation2) return true;
	if(!meet){
		if(!captureAnnotation1||!captureAnnotation2) return true;
		if(captureAnnotation1==CaptureAnnotation.spent||captureAnnotation2==CaptureAnnotation.spent) return false;
		return true; // const, moved, once are intercombinable
	}else{
		// if(!captureAnnotation1||!captureAnnotation2) return true; // TODO?
		if(!captureAnnotation1||!captureAnnotation2) return false;
		if(captureAnnotation1==CaptureAnnotation.spent||captureAnnotation2==CaptureAnnotation.spent) return false;
		if(captureAnnotation1==CaptureAnnotation.once||captureAnnotation2==CaptureAnnotation.once) return true;
		return false; // TODO: combine `const` and `moved` to `none`?
	}
}
CaptureAnnotation combineCaptureAnnotation(CaptureAnnotation captureAnnotation1,CaptureAnnotation captureAnnotation2,bool meet)in{
	assert(captureAnnotationCombinable(captureAnnotation1,captureAnnotation2,meet));
}do{
	if(captureAnnotation1==captureAnnotation2) return captureAnnotation1;
	if(!meet){
		if(!captureAnnotation1) return captureAnnotation2;
		if(!captureAnnotation2) return captureAnnotation1;
		assert(captureAnnotation1!=CaptureAnnotation.spent&&captureAnnotation2!=CaptureAnnotation.spent);
		return CaptureAnnotation.once;
	}else{
		if(!captureAnnotation1||!captureAnnotation2) return CaptureAnnotation.none;
		assert(captureAnnotation1!=CaptureAnnotation.spent&&captureAnnotation2!=CaptureAnnotation.spent);
		assert(captureAnnotation1==CaptureAnnotation.once||captureAnnotation2==CaptureAnnotation.once);
		if(captureAnnotation1==CaptureAnnotation.once) return captureAnnotation2;
		if(captureAnnotation2==CaptureAnnotation.once) return captureAnnotation1;
		assert(0);
	}
}

string annotationToString(Annotation annotation){
	static if(language==silq) return annotation?text(annotation):"";
	static if(language==psi){
		final switch(annotation){
			case Annotation.none: return "";
			case Annotation.pure_: return "pure";
		}
	}
}

class ProductTy: Type{
	Parameter[] params;
	bool[] isConst;
	Id[] names;
	Expression dom, cod; // `dom` set by semantic analysis
	bool isSquare,isTuple;
	CaptureAnnotation captureAnnotation;
	Annotation annotation;
	static if(language==silq){
		private ProductTy classicalTy;
		bool isClassical_;
	}else enum isClassical_=true;
	this(Parameter[] params, Expression cod, bool isSquare, bool isTuple, CaptureAnnotation captureAnnotation, Annotation annotation, bool isClassical_)in{
		assert(cod);
		// TODO: assert that all names are distinct
	}do{
		this.params = params;
		this.isConst = params.map!(p => p.isConst).array;
		this.names = params.map!(p => p.name ? p.getId : Id()).array;
		this.isSquare = isSquare;
		this.isTuple = isTuple;
		this.cod = cod;
		this.captureAnnotation = isClassical_&&captureAnnotation==CaptureAnnotation.const_?CaptureAnnotation.none:captureAnnotation;
		this.annotation = annotation;
		static if(language==silq){
			this.isClassical_=isClassical_||captureAnnotation==CaptureAnnotation.none;
		}
	}
	override void setSemCompleted() {
		if(!isSemError()){
			assert(dom && dom.isSemEvaluated(), format("completed semantic analysis of product type without domain: %s", this));
			assert(cod && cod.isSemCompleted(), format("completed semantic analysis of product type without codomain: %s", this));
		}
		super.setSemCompleted();
	}
	override ProductTy copyImpl(CopyArgs args){
		auto r = new ProductTy(params.map!(p=>p.copy(args)).array, cod.copy(args), isSquare, isTuple, captureAnnotation, annotation, isClassical_);
		if(args.preserveSemantic) {
			r.dom = dom;
		}
		return r;
	}
	/+private+/ @property ITupleTy tdom()in{ // TODO: make private
		assert(isTuple);
		assert(dom);
	}do{
		auto r=dom.isTupleTy;
		assert(!!r);
		return r;
	}
	override string toString(){
		auto c=cod ? cod.toString() : "<missing codomain>";
		auto del=isSquare?"[]":"()";
		string getParamKind(bool const_){
			string paramKind=null;
			static if(language==silq){
				if(const_&&!isSquare) paramKind="const ";
				if(!const_&&isSquare) paramKind="moved ";
			}
			return paramKind;
		}
		string r;
		if(cod && !cod.hasAnyFreeVar(names) && params.all!(p=>p.vtype||p.dtype)){
			string d;
			string addp(bool const_,Expression a,string del="()"){
				auto paramKind=getParamKind(const_);
				if(cast(ProductTy)a) return del[0]~(paramKind?paramKind~"(":"")~a.toString()~(paramKind?")":"")~del[1];
				if(a.isTupleTy()) return (paramKind?paramKind~"(":"")~a.toString()~(paramKind?")":"");
				return paramKind~a.toString();
			}
			d=params.empty?(dom?dom.toString():"𝟙"):params.map!((p){
				auto paramKind=getParamKind(p.isConst);
				auto pty = p.vtype ? p.vtype : p.dtype;
				auto ptup = pty.isTupleTy();
				return (ptup && ptup.length > 1) ? "("~paramKind~pty.toString()~")" : addp(p.isConst, pty);
			}).join(" × ");
			if(isTuple&&params.length==1){
				d="("~d~")¹";
			}
			static if(language==silq) auto arrow=(isClassical_?"!":"")~"→";
			else enum arrow="→";
			if(isSquare) d=del[0]~d~del[1];
			r=d~" "~(captureAnnotation!=CaptureAnnotation.const_?captureAnnotationToString(captureAnnotation):"")~arrow~(annotation?annotationToString(annotation):"")~" "~c;
		}else{
			string args;
			args=params.map!((p){
				auto paramKind=getParamKind(p.isConst);
				auto pty = p.vtype ? p.vtype : p.dtype;
				return paramKind~(p.name ? p.name.toString() : "_")~(pty ? ":"~pty.toString() : "");
			}).join(",");
			if(isTuple&&params.length==1){
				args~=",";
			}
			static if(language==silq) auto pi=(isClassical_?"!":"")~"∏";
			else enum pi="Π";
			r=pi~del[0]~args~del[1]~(captureAnnotation!=CaptureAnnotation.const_?captureAnnotationToString(captureAnnotation):"")
				~(captureAnnotation!=CaptureAnnotation.const_&&annotation?" ":"")~annotationToString(annotation)~". "~c;
		}
		return r;
	}
	override bool isConstant(){ return dom.isConstant() && cod.isConstant(); }
	override bool isTotal(){ return dom.isTotal() && cod.isTotal(); }
	@property size_t nargs(){
		return params.length;
	}
	Expression argTy(size_t i){
		auto ty = params[i].vtype;
		assert(ty.isSemEvaluated());
		return ty;
	}
	bool argConst(size_t i){
		return params[i].isConst;
	}
	bool argConstForReverse(size_t i){
		if(argConst(i)) return true;
		auto ty = argTy(i);
		return ty.isClassical() && !ty.mayBeQuantum();
	}
	bool argConstForSubtyping(size_t i){
		return argConst(i) || argTy(i).isClassical;
	}
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		if(dom) {
			if(auto r=dom.freeVarsImpl(dg)) return r;
		} else {
			assert(!isSemCompleted());
		}
		return cod.freeVarsImpl(v=>names.canFind(v.id)?0:dg(v));
	}
	private ProductTy relabel(Id oname,Id nname)in{
		assert(names.canFind(oname));
		assert(!hasFreeVar(nname));
		assert(!names.canFind(nname));
	}out(r){
		if(oname&&oname!=nname){
			assert(r.names.canFind(nname));
			assert(!r.names.canFind(oname));
		}
	}do{
		if(!oname||oname==nname) return this;
		import std.algorithm;
		auto i=names.countUntil(oname);
		assert(i!=-1);
		auto nnames=names.dup;
		nnames[i]=nname;
		auto nvar=varTy(nname,argTy(i));
		return productTy(isConst,nnames,dom,cod.substitute(oname,nvar),isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
	private ProductTy relabelAway(Id oname)in{
		assert(names.canFind(oname));
	}out(r){
		if(!!oname) assert(!r.names.canFind(oname));
	}do{
		if(!oname) return this;
		auto nname=oname;
		while(names.canFind(nname)||hasFreeVar(nname)) nname=nname.apos;
		return relabel(oname,nname);
	}
	private Id freshName(Id base,Expression block){
		auto nn=base;
		if(!nn) nn=Id.intern("x");
		while(hasFreeVar(nn)||block.hasFreeVar(nn)) nn=nn.apos;
		return nn;
	}
	Id[] freshNames(Expression block){
		Expression[] mentions=[block];
		static if(language==silq) foreach(e;only(isType(block)?block:null,block.type)) if(e){ // (and the values of the type variables that it mentions, through which the unification looks, e.g., `n` for an argument of type `t` after `t:=uint[n]`, see `unfoldTypeVariables`)
			auto u=unfoldTypeVariables(e);
			if(u !is e) mentions~=u;
		}
		auto nnames=names.dup;
		foreach(i,ref nn;nnames){
			if(!nn) nn=Id.intern("x");
			while(hasFreeVar(nn)||mentions.any!(e=>e.hasFreeVar(nn))||nnames[0..i].canFind(nn)) nn=nn.apos;
		}
		return nnames;
	}
	ProductTy relabelAll(Id[] nnames)out(r){
		assert(nnames.length==names.length);
		foreach(n;nnames) assert(!hasFreeVar(n));
	}do{
		if(nnames==names) return this;
		MapSX!(Id,Expression) subst;
		foreach(i;0..names.length) subst[names[i]]=varTy(nnames[i],argTy(i));
		return productTy(isConst,nnames,dom,cod.substitute(subst),isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
	override ProductTy substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		foreach(n;names){
			if(!n) continue;
			bool ok=true;
			foreach(k,v;subst) if(v.hasFreeVar(n)) ok=false;
			if(ok) continue;
			auto r=cast(ProductTy)relabelAway(n).substitute(subst,tt);
			assert(!!r);
			return r;
		}
		auto ndom=dom.substitute(subst,tt);
		auto nsubst=subst.dup;
		foreach(n;names) nsubst.remove(n);
		auto ncod=cod.substitute(nsubst,tt);
		return productTy(isConst,names,ndom,ncod,isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		auto r=cast(ProductTy)rhs; // TODO: get rid of duplication (same code in opEquals)
		if(!r) return false;
		if(isTuple&&!r.dom.isTupleTy()) return false;
		r=r.setTuple(isTuple);
		if(!r) return false;
		if(isConst.length!=r.isConst.length) return false;
		if(isSquare!=r.isSquare||annotation>r.annotation||!captureAnnotationSubtype(r.captureAnnotation,captureAnnotation)||
		   isClassical_&&!r.isClassical_||nargs!=r.nargs)
			return false;
		foreach(name;names){
			if(r.hasFreeVar(name))
				return relabelAway(name).unify(r,subst,meet);
		}
		foreach(name;r.names){
			if(hasFreeVar(name))
				return unify(r.relabelAway(name),subst,meet);
		}
		// assert(!names.any!(name=>r.hasFreeVar(name)));
		// assert(!r.names.any!(name=>hasFreeVar(name)));
		r=r.relabelAll(iota(names.length).map!(i=>names[i]?names[i]:r.names[i]).array);
		MapSX!(Id,UnificationResult) nsubst;
		foreach(k,v;subst) if(!names.canFind(k)) nsubst[k]=v;
		auto res=dom.unify(r.dom,nsubst,!meet)&&cod.unify(r.cod,nsubst,meet);
		foreach(k,v;nsubst) subst[k]=v;
		return res;
	}
	Expression tryMatch(Expression arg,out Expression garg,Scope target=null)in{assert(isSquare&&cast(ProductTy)cod);}do{
		auto cod=cast(ProductTy)this.cod;
		assert(!!cod);
		auto nnames=freshNames(arg);
		if(nnames!=names) return relabelAll(nnames).tryMatch(arg,garg);
		Expression[] atys;
		auto tpl=arg.type.isTupleTy();
		if(cod.isTuple&&tpl){
			atys=iota(tpl.length).map!(i=>tpl[i]).array;
			if(atys.length!=cod.nargs) return null;
		}else atys=[arg.type];
		MapSX!(Id,UnificationResult) subst;
		foreach(i,n;names) subst[n]=UnificationResult.init;
		foreach(i,aty;atys){
			if(i>=cod.nargs) continue;
			if(!cod.argTy(i).unify(aty,subst,false))
				return null;
		}
		auto gargs=new Expression[](names.length);
		foreach(i,n;names){
			Expression value=null;
			if(auto low=subst[n].bound(false)){
				if(argTy(i)==qtypeTy||isQNumericTy(argTy(i)))
					low=low.getQuantum();
				if(low&&!value) value=low;
			}
			if(auto high=subst[n].bound(true)){
				if(argTy(i)==ctypeTy)
					high=high.getClassical();
				else if(isQNumericTy(argTy(i)))
					high=high.getQuantum();
				if(high&&!value) value=high;
			}
			if(!value) return null;
			gargs[i]=value;
		}
		if(!isTuple) assert(gargs.length==1);
		if(isTuple){
			auto tgarg=new TupleExp(gargs);
			tgarg.type=tupleTy(gargs.map!(garg=>garg.type).array);
			tgarg.setSemCompleted();
			garg=tgarg;
		}else garg=gargs[0];
		cod=cast(ProductTy)tryApply(garg,true);
		if(!cod) return null;
		return cod.tryApply(arg,false,target);
	}
	Expression tryMatchReverse(Expression arg,Expression resultTy,out Expression garg)in{assert(isSquare&&cast(ProductTy)cod);}do{
		auto cod=cast(ProductTy)this.cod;
		assert(!!cod);
		auto nnames=freshNames(arg);
		if(nnames!=names) return relabelAll(nnames).tryMatchReverse(arg,resultTy,garg);
		Expression[] args;
		auto tpl=cast(TupleExp)arg;
		if(cod.isTuple&&tpl){
			if(tpl.length!=cod.nargs) return null;
			args=tpl.e;
		}else args=[arg];
		MapSX!(Id,UnificationResult) subst;
		foreach(i,n;names) subst[n]=UnificationResult.init;
		if(resultTy&&!cod.cod.hasAnyFreeVar(cod.names))
			if(!cod.cod.unify(resultTy,subst,false))
				return null;
		auto fromResult=names.map!(n=>!!subst[n].bound(false)||!!subst[n].bound(true)).array;
		foreach(i,a;args){
			if(i>=cod.nargs) continue;
			if(!cod.isConstForReverse[i]) continue;
			if(!a.type||!cod.argTy(i).unify(a.type,subst,false))
				return null;
		}
		foreach(i,n;names){
			if(fromResult[i]||!isTypeTy(argTy(i))) continue;
			foreach(j;0..cod.nargs)
				if(!cod.isConstForReverse[j]&&cod.argTy(j).hasFreeVar(n))
					return null;
		}
		auto gargs=new Expression[](names.length);
		foreach(i,n;names){
			Expression value=null;
			if(auto low=subst[n].bound(false)){
				if(argTy(i)==qtypeTy||isQNumericTy(argTy(i)))
					low=low.getQuantum();
				if(low&&!value) value=low;
			}
			if(auto high=subst[n].bound(true)){
				if(argTy(i)==ctypeTy)
					high=high.getClassical();
				else if(isQNumericTy(argTy(i)))
					high=high.getQuantum();
				if(high&&!value) value=high;
			}
			if(!value) return null;
			gargs[i]=value;
		}
		if(!isTuple) assert(gargs.length==1);
		if(isTuple){
			auto tgarg=new TupleExp(gargs);
			tgarg.type=tupleTy(gargs.map!(garg=>garg.type).array);
			tgarg.setSemCompleted();
			garg=tgarg;
		}else garg=gargs[0];
		auto r=tryApply(garg,true);
		if(auto inst=cast(ProductTy)r)
			foreach(j;0..inst.nargs)
				if(!inst.isConst[j]&&inst.argTy(j).hasClassicalComponent()) // TODO: fix
					return null;
		return r;
	}
	Expression tryApply(Expression arg,bool isSquare,Scope target=null){
		assert(arg.isSemCompleted());
		if(isSquare != this.isSquare) return null;
		if(!isSubtype(arg.type,dom)) return null;
		return applyUnchecked(arg,target);
	}
	private Expression applyUnchecked(Expression arg,Scope target){
		MapSX!(Id,Expression) subst;
		if(isTuple){
			auto targTy=arg.type.isTupleTy();
			if(!targTy) return null; // (arg.type may be ⊥)
			assert(!!tdom);
			auto targ=cast(TupleExp)arg;
			if(targ&&targ.length==names.length){
				foreach(i,n;names) subst[n]=targ.e[i].eval();
			}else{
				foreach(i,n;names){
					auto exp=new IndexExp(arg,LiteralExp.makeInteger(i));
					exp.type=targTy[i];
					exp.setSemCompleted();
					subst[n]=exp.eval();
				}
			}
		}else{
			assert(names.length==1);
			subst[names[0]]=arg.eval();
		}
		// the codomain moves from the expression context of the callee into a
		// type used at the call site; transition it to the type context first
		import ast.substitute: transitionToType;
		return transitionToType(cod,target).substitute(subst);
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		auto r=cast(ProductTy)rhs;
		if(!r) return false;
		if(isTuple&&!r.dom.isTupleTy()) return false;
		r=r.setTuple(isTuple);
		if(!r) return false;
		assert(isTuple==r.isTuple);
		if(isConst!=r.isConst||isSquare!=r.isSquare||annotation!=r.annotation||captureAnnotation!=r.captureAnnotation||
		   isClassical_!=r.isClassical_||nargs!=r.nargs)
			return false;
		auto flipped=ctx.flipped();
		return this.isSubtypeImpl(r,&ctx)&&r.isSubtypeImpl(this,&flipped);
	}
	auto isConstForReverse(){
		return iota(nargs).map!(i=>argConstForReverse(i));
	}
	private auto isConstForSubtyping(){
		return iota(nargs).map!(i=>argConstForSubtyping(i));
	}

	bool isConstCompatible(ProductTy rhs){
		assert(isTuple == rhs.isTuple);
		assert(nargs == rhs.nargs);
		return iota(nargs).all!(i =>
			argConst(i) == rhs.argConst(i) ||
			argTy(i).isClassical || rhs.argTy(i).isClassical
		);
	}

	override bool isSubtypeImpl(Expression rhs,EqualityContext* ctx){
		auto r=cast(ProductTy)rhs;
		if(!r) return false;
		if(isTuple&&!r.dom.isTupleTy()) return false;
		r=r.setTuple(isTuple);
		if(!r) return false;
		if(isSquare!=r.isSquare||nargs!=r.nargs||!isConstCompatible(r))
			return false;
		if(annotation<r.annotation||!captureAnnotationSubtype(captureAnnotation,r.captureAnnotation)||!isClassical_&&r.isClassical_)
			return false;
		auto name=freshName(Id(),r);
		auto vars=varTy(name,r.dom);
		if(ctx){
			auto flipped=ctx.flipped(); // (the domain is contravariant)
			if(!isSubtype(r.dom,dom,&flipped)) return false;
		}else if(!isSubtype(r.dom,dom)) return false;
		auto lCod=applyUnchecked(vars,null);
		auto rCod=r.applyUnchecked(vars,null);
		if(!lCod) return false;
		assert(!!rCod);
		return isSubtype(lCod,rCod,ctx);
	}
	override Expression combineTypesImpl(Expression rhs,bool meet){
		auto r=cast(ProductTy)rhs;
		if(!r) return null;
		if(!captureAnnotationCombinable(captureAnnotation,r.captureAnnotation,meet)) return null;
		CaptureAnnotation ncaptureAnnotation;
		// ignore const classical captures for combining capture annotations:
		auto classicalConst1=isClassical_&&captureAnnotation==CaptureAnnotation.const_;
		auto classicalConst2=r.isClassical_&&r.captureAnnotation==CaptureAnnotation.const_;
		if(classicalConst1&&classicalConst2) ncaptureAnnotation=CaptureAnnotation.const_;
		else if(classicalConst1) ncaptureAnnotation=r.captureAnnotation;
		else if(classicalConst2) ncaptureAnnotation=captureAnnotation;
		else ncaptureAnnotation=combineCaptureAnnotation(captureAnnotation,r.captureAnnotation,meet);
		auto nannotation=meet?max(annotation,r.annotation):min(annotation,r.annotation);
		auto nisClassical=meet?isClassical_||r.isClassical_:isClassical_&&r.isClassical_;
		auto ndom=combineTypes(dom,r.dom,!meet);
		if(!ndom) return null;
		auto tpl=isTuple?ndom.isTupleTy():null;
		if(isTuple!=r.isTuple||isTuple&&!tpl||isTuple&&names!=r.names){
			auto nl=setTuple(false);
			auto nr=r.setTuple(false);
			if(!nl||!nr) return null;
			return combineTypes(nl,nr,meet);
		}
		if(!equal(isConstForSubtyping,r.isConstForSubtyping)||isSquare!=r.isSquare||nargs!=r.nargs)
			return null;
		auto nIsConst=isConst==r.isConst?isConst:zip(isConst,r.isConst).map!(x=>x[0]&&x[1]).array;
		if(isTuple){
			assert(names==r.names);
			assert(!!tpl);
			if(tpl.length!=names.length) return null;
			auto vars=new TupleExp(iota(names.length).map!(i=>cast(Expression)varTy(names[i],tpl[i])).array);
			vars.type=ndom;
			vars.setSemCompleted();
			auto lCod=tryApply(vars,isSquare);
			auto rCod=r.tryApply(vars,isSquare);
			if(!lCod||!rCod) return null;
			auto ncod=combineTypes(lCod,rCod,meet);
			if(!ncod) return null;
			return productTy(nIsConst,names,ndom,ncod,isSquare,isTuple,ncaptureAnnotation,nannotation,nisClassical);
		}else{
			Expression lCod,rCod;
			auto nnames=this.names;
			if(names[0]!=Id()||r.names[0]!=Id()){
				auto name=nnames[0];
				if(names[0]!=r.names[0]){
					name=freshName(Id(),r);
					nnames=[name];
				}
				auto var=varTy(name,ndom);
				lCod=tryApply(var,isSquare);
				rCod=r.tryApply(var,isSquare);
			}else{
				lCod=cod;
				rCod=r.cod;
			}
			if(!lCod||!rCod) return null;
			auto ncod=combineTypes(lCod,rCod,meet);
			if(!ncod) return null;
			return productTy(nIsConst,nnames,ndom,ncod,isSquare,isTuple,ncaptureAnnotation,nannotation,nisClassical);
		}
	}
	final ProductTy setCaptureAnnotation(CaptureAnnotation captureAnnotation){
		return productTy(isConst,names,dom,cod,isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
	final ProductTy setAnnotation(Annotation annotation){
		return productTy(isConst,names,dom,cod,isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
	ProductTy setTuple(bool tuple)in{
		assert(!tuple||dom.isTupleTy());
	}do{
		if(tuple==isTuple) return this;
		Id[] nnames;
		bool[] nIsConst;
		if(tuple){
			auto tpl=dom.isTupleTy();
			assert(!!tpl);
			assert(!isTuple&&names.length==1);
			nnames=iota(tpl.length).map!(i=>Id.intern(names[0].str~lowNum(i))).array;
			assert(isConst.length==1);
			nIsConst=isConst[0].repeat(tpl.length).array;
		}else{
			if(!isConst.empty&&!isConst.all!(x=>x==isConst.front))
				return null;
			nnames=[Id.intern("t")];
			nIsConst=[isConst.empty?false:isConst.front];
		}
		foreach(i,ref nn;nnames) while(hasFreeVar(nn)) nn=nn.apos;
		Expression narg;
		if(tuple){
			auto tpl=dom.isTupleTy();
			assert(!!tpl);
			assert(!isTuple&&names.length==1);
			auto vars=new TupleExp(iota(nnames.length).map!(i=>cast(Expression)varTy(nnames[i],tpl[i])).array);
			vars.type=dom;
			vars.setSemCompleted();
			narg=vars;
		}else{
			assert(isTuple&&nnames.length==1);
			narg=varTy(nnames[0],dom);
		}
		auto ncod=tryApply(narg,isSquare);
		assert(!!ncod);
		return productTy(nIsConst,nnames,dom,ncod,isSquare,tuple,captureAnnotation, annotation,isClassical(this));
	}
	override ProductTy getClassical(){
		static if(language==silq) {
			if(classicalTy) return classicalTy;
			if(isClassical_) return classicalTy=this;
			return classicalTy=productTy(isConst, names, dom, cod, isSquare, isTuple, captureAnnotation, annotation, true);
		} else {
			return this;
		}
	}
	override int componentsImpl(scope int delegate(Expression) e){
		return 0; // TODO: ok?
	}
	override Expression evalImpl(){
		assert(isTypeTy(type));
		auto ndom=dom;
		auto ncod=cod.eval();
		return productTy(isConst,names,ndom,ncod,isSquare,isTuple,captureAnnotation,annotation,isClassical_);
	}
}

ProductTy productTy(bool[] isConst,Id[] names,Expression dom,Expression cod,bool isSquare,bool isTuple,CaptureAnnotation captureAnnotation,Annotation annotation,bool isClassical)in{
	assert(dom && dom.isSemEvaluated(), format("function domain not analyzed: %s", dom));
	assert(cod && cod.isSemEvaluated());
	if(isTuple){
		auto tdom=dom.isTupleTy();
		assert(tdom&&names.length==tdom.length&&isConst.length==tdom.length);
	}else assert(names.length==1&&isConst.length==1);
}do{
	return memoize!((bool[] isConst,Id[] names,Expression dom,Expression cod,bool isSquare,bool isTuple,CaptureAnnotation captureAnnotation, Annotation annotation,bool isClassical){
		Expression[] types;
		if(isTuple) {
			auto tdom = dom.isTupleTy;
			assert(tdom);
			types = iota(tdom.length).map!(i => tdom[i]).array;
		} else {
			types = [dom];
		}
		assert(types.length == names.length);
		auto params = new Parameter[names.length];
		MapSX!(Id,Expression) subst;
		foreach(i, name; names) {
			Identifier id;
			if(name) {
				id = varTy(name, types[i]);
				if(name) subst[name] = id;
			}
			auto p = new Parameter(isConst[i], id, types[i]);
			params[i] = p;
			p.vtype = p.dtype;
			p.setSemEvaluated();
		}
		cod = cod.substitute(subst);
		auto r = new ProductTy(params, cod, isSquare, isTuple, captureAnnotation, annotation, isClassical);
		r.dom = dom;
		r.type = typeOfProductTy(isConst, names, dom, cod, isSquare, isTuple, captureAnnotation, annotation, isClassical);
		r.setSemEvaluated();
		return r;
	})(isConst, names, dom, cod, isSquare, isTuple, captureAnnotation, annotation, isClassical);
}

alias FunTy=ProductTy;
FunTy funTy(bool[] isConst,Expression dom,Expression cod,bool isSquare,bool isTuple,Annotation annotation,bool isClassical)in{
	assert(dom&&cod);
	if(isTuple){
		auto tdom=dom.isTupleTy();
		assert(tdom&&isConst.length==tdom.length);
	}else assert(isConst.length==1);
}do{
	auto nargs=1+[].length;
	if(isTuple) if(auto tpl=dom.isTupleTy()) nargs=tpl.length;
	return productTy(isConst,iota(nargs).map!(_=>Id()).array,dom,cod,isSquare,isTuple,CaptureAnnotation.const_,annotation,isClassical);
}

FunTy funTy(Expression dom,Expression cod,bool isSquare,bool isTuple,Annotation annotation,bool isClassical)in{
	assert(dom&&cod);
}do{
	auto nargs=1+[].length;
	if(isTuple) if(auto tpl=dom.isTupleTy()) nargs=tpl.length;
	return funTy(false.repeat(nargs).array,dom,cod,isSquare,isTuple,annotation,isClassical);
}

FunTy funTy(Expression dom,Expression cod,bool isSquare,bool isTuple,bool isClassical)in{
	assert(dom&&cod);
}do{
	return funTy(dom,cod,isSquare,isTuple,pure_,isClassical);
}

Expression typeOfVariadicTy(Expression next, bool isClassical)in{
	assert(next&&next.type,text(next));
	if(auto tpl=cast(TupleTy)next.type)
		assert(tpl.types.all!(t=>isType(t)||isQNumeric(t)));
	else{
		auto et=elementType(next.type);
		assert(isType(et)||isQNumeric(et));
	}
}do{
	if(auto tpl=cast(TupleTy)next.type){
		Expression r=utypeTy;
		foreach(t;tpl.types)
			r=joinTypes(r,t);
		return isClassical ? r.getClassicalTy() : r;
	}
	auto enext=elementType(next.type);
	return isClassical ? enext.getClassicalTy() : enext;
}

class VariadicTy: Type{
	Expression next;
	bool isClassical_;
	override ITupleTy isTupleTy(){
		auto r=eval();
		if(cast(VariadicTy)r) return null;
		return r.isTupleTy();
	}
	this(Expression next,bool isClassical_){
		this.next=next;
		this.isClassical_=isClassical_;
	}
	override VariadicTy copyImpl(CopyArgs args){
		return new VariadicTy(next.copy(args), isClassical_);
	}
	override string toString(){
		auto ns="("~next.toString()~")";
		import std.uni:isAlpha;
		return (isClassical_?"!":"")~(ns[0].isAlpha?"∏ ":"∏")~ns;
	}
	override bool isConstant(){ return next.isConstant(); }
	override bool isTotal(){ return next.isTotal(); }
	override int freeVarsImpl(scope int delegate(Identifier) dg){
		return next.freeVarsImpl(dg);
	}
	override Expression substituteImpl(MapSX!(Id,Expression) subst,TypeTransition* tt){
		return variadicTy(next.substitute(subst,tt),isClassical_);
	}
	override bool unifyImpl(Expression rhs,ref MapSX!(Id,UnificationResult) subst,bool meet){
		if(auto vt=cast(VariadicTy)rhs)
			return next.unify(vt.next,subst,meet);
		// if(auto vt=cast(VectorTy)rhs) return next.unify(vector(vt.next.num,vt.next.type),subst,meet); // TODO
		// if(auto at=cast(ArrayTy)rhs) // TODO
		if(auto tt=rhs.isTupleTy()){
			auto types=iota(tt.length).map!(i=>tt[i]).array;
			if(auto id=cast(Identifier)next){
				if(id.id in subst){
					if(auto bound=subst[id.id].bound(meet)){
						if(auto cmb=combineTypeLists(bound,types,meet)){
							auto ur=subst[id.id];
							if(meet) ur.upperBound=cmb;
							else ur.lowerBound=cmb;
							subst[id.id]=ur;
							return true;
						}
					}
				}
			}
			return next.unify(typeList(types),subst,meet);
		}
		return false;
	}
	private static TupleExp typeList(Expression[] types){
		auto tpl=new TupleExp(types);
		tpl.type=tupleTy(tpl.e.map!(e=>e.type).array);
		tpl.setSemCompleted();
		return tpl;
	}
	private static TupleExp combineTypeLists(Expression bound,Expression[] types,bool meet){
		Expression[] bs;
		if(auto tpl=cast(TupleExp)bound) bs=tpl.e;
		else if(auto vec=cast(VectorExp)bound) bs=vec.e;
		else return null;
		if(bs.length!=types.length) return null;
		Expression[] cs;
		foreach(i;0..bs.length){
			if(!(isType(bs[i])||isQNumeric(bs[i]))) return null;
			auto c=combineTypes(bs[i],types[i],meet);
			if(!c) return null;
			cs~=c;
		}
		return typeList(cs);
	}
	override Expression evalImpl(){
		assert(isTypeTy(type));
		auto ne=next.eval();
		bool hasElements=false;
		Expression[] elements;
		if(auto vec=cast(VectorExp)ne){
			hasElements=true;
			elements=vec.e;
		}
		if(auto tpl=cast(TupleExp)ne){
			hasElements=true;
			elements=tpl.e;
		}
		if(hasElements){
			auto tt=tupleTy(elements);
			if(isClassical_) return tt.getClassical;
			return tt;
		}
		if(auto r=reduce(ne)){
			if(isClassical_) if(auto cr=r.getClassical()) return cr;
			return r;
		}
		if(ne is next) return this;
		return variadicTy(ne,isClassical_);
	}
	private static Expression reduce(Expression list){
		Expression n,x;
		if(isVectorCall(list,n,x)){
			if((isType(x)||isQNumeric(x))&&n.type&&isSubtype(n.type,ℕt(true)))
				return vectorTy(x,n);
			return null;
		}
		if(auto cat=cast(CatExp)list){
			auto l=variadicTy(cat.e1,false).eval(), r=variadicTy(cat.e2,false).eval();
			auto lv=cast(VectorTy)l, rv=cast(VectorTy)r;
			if(lv&&rv&&lv.next==rv.next){
				auto num=new AddExp(lv.num,rv.num);
				num.type=ℕt(true);
				num.loc=cat.loc;
				num.setSemCompleted();
				return vectorTy(lv.next,num.eval());
			}
			auto lt=l.isTupleTy(), rt=r.isTupleTy();
			if(lt&&rt&&!cast(VariadicTy)l&&!cast(VariadicTy)r){
				Expression[] types;
				foreach(i;0..lt.length) types~=lt[i];
				foreach(i;0..rt.length) types~=rt[i];
				return tupleTy(types);
			}
		}
		return null;
	}
	private static bool isVectorCall(Expression e,out Expression n,out Expression x){
		auto ce=cast(CallExp)e;
		if(!ce||ce.isSquare) return false;
		Identifier id=cast(Identifier)ce.e;
		if(auto sce=cast(CallExp)ce.e) if(sce.isSquare) id=cast(Identifier)sce.e;
		if(!id||!id.meaning) return false;
		import ast.semantic_:isPreludeSymbol;
		if(isPreludeSymbol(id.meaning)!="vector") return false;
		auto tpl=cast(TupleExp)ce.arg;
		if(!tpl||tpl.length!=2) return false;
		n=tpl.e[0];
		x=tpl.e[1];
		return true;
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		if(auto r=cast(VariadicTy)rhs)
			return isEqual(next,r.next,&ctx)&&isClassical_==r.isClassical;
		return false;
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		if(auto vt=cast(VariadicTy)r)
			return isEqual(next,vt.next,ctx) && isClassical(this)>=isClassical(vt); // TODO: improve
		// if(auto vt=cast(VectorTy)rhs) ... // TODO
		// if(auto at=cast(ArrayTy)rhs) ... // TODO
		if(auto tt=r.isTupleTy()){
			auto tpl=new TupleExp(iota(tt.length).map!(i=>tt[i]).array);
			tpl.type=tupleTy(iota(tt.length).map!(i=>tt[i].type).array);
			tpl.setSemCompleted();
			return isEqual(next,tpl,ctx); // TODO: improve
		}
		return false;
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		if(this==r) return this;
		if(auto vt=cast(VariadicTy)r){
			if(!isEqual(next,vt.next,null)) return null; // TODO: combine elementwise
			bool classical=meet?isClassical_||vt.isClassical_:isClassical_&&vt.isClassical_;
			return variadicTy(next,classical);
		}
		return null; // TODO
	}
	override Expression getClassical(){
		if(isClassical_) return this;
		return variadicTy(next, true);
	}
	override Expression getQuantum(){
		return null; // TODO
	}
	override bool mayBeClassical(){ return true; } // TODO
	override bool mayBeQuantum(){ return true; } // TODO
	override int componentsImpl(scope int delegate(Expression) dg){
		return dg(next);
	}
}

Expression variadicTy(Expression next,bool isClassical)in{
	assert(next&&next.isSemEvaluated());
	if(auto tpl=cast(TupleTy)next.type)
		assert(tpl.types.all!(t=>isType(t)||isQNumeric(t)));
	else assert(isType(elementType(next.type))||isQNumeric(elementType(next.type)));
}do{
	if(auto ve=cast(VectorExp)next){
		next=new TupleExp(ve.e);
		next.type=tupleTy(ve.e.map!(e=>e.type).array);
		next.setSemCompleted();
		next=next.eval();
	}
	return memoize!((Expression next,bool isClassical){
		auto r = new VariadicTy(next, isClassical);
		r.type = typeOfVariadicTy(next, isClassical);
		r.setSemCompleted();
		assert(!r.isClassical_ || r.type.isClassical);
		return r;
	})(next,isClassical).eval();
}

Identifier varTy(Id name,Expression type,bool classical=false)in{
	assert(name&&type);
}do{
	return memoize!((Id name,Expression type,bool classical){
		auto r=new Identifier(name);
		static if(language==silq) r.classical=classical;
		r.type=type;
		r.setSemEvaluated();
		return r;
	})(name,type,classical);
}

struct FreeIdentifiers{
	Expression self;
	int opApply(scope int delegate(Identifier) dg){
		int rec(Expression e){
			if(auto id=cast(Identifier)e) return dg(id);
			if(auto pt=cast(ProductTy)e){
				foreach(id;pt.dom.freeIdentifiers)
					if(auto r=dg(id)) return r;
				foreach(id;pt.cod.freeIdentifiers){
					if(pt.names.canFind(id.id)) continue;
					if(auto r=dg(id)) return r;
				}
				return 0;
			}
			// statements bind local variables that are not free in the overall expression
			import ast.substitute:blockFreeVarsImpl,functionDefFreeVarsImpl,blockFreeVarsImpl;
			if(auto le=cast(LetExp)e) return blockFreeVarsImpl(le.s.s,le.e,dg);
			if(auto lam=cast(LambdaExp)e) return functionDefFreeVarsImpl(lam.fd,dg);
			if(auto fd=cast(FunctionDef)e) return functionDefFreeVarsImpl(fd,dg);
			if(auto ce=cast(CompoundExp)e) return blockFreeVarsImpl(ce.s,null,dg);
			foreach(x;e.components)
				if(auto r=rec(x))
					return r;
			return 0;
		}
		return rec(self);
	}
}
auto freeIdentifiers(Expression self){
	return FreeIdentifiers(self);
}
bool hasFreeIdentifier(Expression self,Id name){
	foreach(id;self.freeIdentifiers) if(id.id==name) return true;
	return false;
}
/// a supertype of `type` that does not mention the variables for which `eliminated` holds, as the join with a type that does not mention them, or `null`
Expression eliminateVariables(Expression type,scope bool delegate(Declaration) eliminated){
	bool mentions(Expression e){
		foreach(id;e.freeIdentifiers) if(id.meaning&&eliminated(id.meaning)) return true;
		return false;
	}
	if(!mentions(type)) return type;
	static if(language==silq){ // (an eliminated type variable stands for its value, see `typeVariableValue`)
		auto u=unfoldTypeVariables(type,eliminated);
		if(u !is type) return eliminateVariables(u,eliminated);
	}
	if(auto vt=cast(VectorTy)type){
		auto next=eliminateVariables(vt.next,eliminated);
		if(!next) return null;
		return mentions(vt.num)?arrayTy(next):vectorTy(next,vt.num);
	}
	if(auto at=cast(ArrayTy)type){
		auto next=eliminateVariables(at.next,eliminated);
		return next?arrayTy(next):null;
	}
	if(auto tt=cast(TupleTy)type){
		Expression[] types;
		foreach(t;tt.types){
			auto w=eliminateVariables(t,eliminated);
			if(!w) return null;
			types~=w;
		}
		return tupleTy(types);
	}
	return null;
}


// kinds (in PSI, all types are classical: `*` denotes `ctype` and `qtype` is not used)
private enum TypeType {
	etype,
	utype,
	ctype,
	qtype,
	mtype,
	badty,
}
private immutable TypeType[5][5] typeJoin = [
	[TypeType.etype, TypeType.ctype, TypeType.ctype, TypeType.mtype, TypeType.mtype],
	[TypeType.ctype, TypeType.utype, TypeType.ctype, TypeType.qtype, TypeType.mtype],
	[TypeType.ctype, TypeType.ctype, TypeType.ctype, TypeType.mtype, TypeType.mtype],
	[TypeType.mtype, TypeType.qtype, TypeType.mtype, TypeType.qtype, TypeType.mtype],
	[TypeType.mtype, TypeType.mtype, TypeType.mtype, TypeType.mtype, TypeType.mtype],
];
private immutable TypeType[5][5] typeMeet = [
	[TypeType.etype, TypeType.badty, TypeType.etype, TypeType.badty, TypeType.etype],
	[TypeType.badty, TypeType.utype, TypeType.utype, TypeType.utype, TypeType.utype],
	[TypeType.etype, TypeType.utype, TypeType.ctype, TypeType.utype, TypeType.ctype],
	[TypeType.badty, TypeType.utype, TypeType.utype, TypeType.qtype, TypeType.qtype],
	[TypeType.etype, TypeType.utype, TypeType.ctype, TypeType.qtype, TypeType.mtype],
];

class TypeTy: Type{
	private TypeType tyty;
	private this(TypeType tyty){
		assert(theTypeTys[tyty] is null, "types are singletons");
		static if(language==psi) assert(tyty!=TypeType.mtype);
		this.tyty = tyty;
		// TODO: types capturing quantum values?
		this.type=(tyty == TypeType.ctype ? this : ctypeTy());
		setSemEvaluated();
	}
	override string toString(){
		final switch(tyty) {
			case TypeType.etype: return "etype";
			case TypeType.utype: return "utype";
			case TypeType.ctype: return language==psi?"*":"ctype";
			case TypeType.qtype: return "qtype";
			case TypeType.mtype: return "*";
			case TypeType.badty: return "null";
		}
	}
	override bool isSubtypeImpl(Expression r,EqualityContext* ctx){
		assert(r !is this);
		auto ty=cast(TypeTy)r;
		if(!ty) return false;
		return typeJoin[this.tyty][ty.tyty] == ty.tyty;
	}
	override Expression combineTypesImpl(Expression r,bool meet){
		assert(r !is this);
		auto ty=cast(TypeTy)r;
		if(!ty) return null;
		return typeTyImpl(meet ? typeMeet[this.tyty][ty.tyty] : typeJoin[this.tyty][ty.tyty]);
	}
	override TypeTy copyImpl(CopyArgs args){
		return this;
	}
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) dg){
		return 0;
	}
}


private TypeTy[5] theTypeTys;
private TypeTy typeTyImpl(TypeType tyty) {
	if(tyty==TypeType.badty) return null;
	static if(language==psi) if(tyty==TypeType.mtype) tyty=TypeType.ctype; // (no quantum types in PSI: `*` is `ctype`, `qtype` is unused)
	return theTypeTys[tyty] ? theTypeTys[tyty] : (theTypeTys[tyty] = new TypeTy(tyty));
}
TypeTy etypeTy(){ return typeTyImpl(TypeType.etype); }
TypeTy utypeTy(){ return typeTyImpl(TypeType.utype); }
TypeTy ctypeTy(){ return typeTyImpl(TypeType.ctype); }
TypeTy qtypeTy(){ return typeTyImpl(TypeType.qtype); }
TypeTy typeTy(){ return typeTyImpl(TypeType.mtype); }

bool isTypeTy(Expression e){ return isSubtype(e,typeTy); }
bool isType(Expression e){ return e&&isTypeTy(e.type); }

bool isEmptyTy(Expression e){ return isSubtype(e,etypeTy); }
bool isEmpty(Expression e){ return e&&isEmptyTy(e.type); }

bool isUnitTy(Expression e){ return isSubtype(e,utypeTy); }
bool isUnit(Expression e){ return e&&isUnitTy(e.type); }

bool isClassicalTy(Expression e){ return isSubtype(e,ctypeTy); }
bool isClassical(Expression e){ return e&&isClassicalTy(e.type); }

bool isQuantumTy(Expression e){
	static if(language==silq) return isSubtype(e,qtypeTy);
	else return false;
}
bool isQuantum(Expression e){ return e&&isQuantumTy(e.type); }

Expression getClassicalTy(Expression e)in{ // typeof(!x) for x:e
	assert(isType(e)||isQNumeric(e));
}do{
	return ctypeTy;
}

bool hasClassicalComponentTy(Expression e){ return !isQuantumTy(e); }
bool hasClassicalComponent(Expression e){ return e&&hasClassicalComponentTy(e.type); }

bool hasQuantumComponentTy(Expression e){ return !isClassicalTy(e); }
bool hasQuantumComponent(Expression e){ return e&&hasQuantumComponentTy(e.type); }

Expression typeOfBoolTy(bool classical){
	return classical?ctypeTy:qtypeTy;
}

class QNumericTy: Type{ // (only used in Silq)
	this(){
		this.type=ctypeTy;
		setSemEvaluated();
	}
	override QNumericTy copyImpl(CopyArgs args){
		return this;
	}
	override string toString(){
		return "qnumeric";
	}
	override bool isEqualImpl(Expression rhs,ref EqualityContext ctx){
		return !!cast(QNumericTy)rhs;
	}
	override Expression evalImpl(){ return this; }
	mixin VariableFree;
	override int componentsImpl(scope int delegate(Expression) dg){
		return 0;
	}
}
private QNumericTy theQNumericTy;
QNumericTy qnumericTy(){ return theQNumericTy?theQNumericTy:(theQNumericTy=new QNumericTy()); }
bool isQNumericTy(Expression e){
	static if(language==silq) return e==qnumericTy;
	else return false;
}
bool isQNumeric(Expression e){ return e&&isQNumericTy(e.type); }

Expression typeOfNumericTy(bool classical){
	if(classical) return ctypeTy;
	static if(language==silq) return qnumericTy;
	else return typeTy;
}

Expression typeOfTupleTy(scope Expression[] e...)in{
	assert(e.all!(e=>isType(e)||isQNumeric(e)));
}do{
	if(!e.length) return utypeTy;
	if(e.any!isEmpty) return etypeTy;
	static if(language==silq){
		if(e.any!isQNumeric) return qnumericTy;
	}
	if(e.all!isUnit) return utypeTy;
	if(e.all!isClassical) return ctypeTy;
	if(e.all!isQuantum) return qtypeTy;
	return typeTy;
}

Expression typeOfArrayTy(Expression e)in{
	assert(isType(e)||isQNumeric(e));
}do{
	static if(language==silq){
		if(isQNumeric(e)) return qnumericTy;
	}
	if(isEmpty(e)) return utypeTy;
	if(isQNumeric(e)) return qnumericTy;
	if(isClassical(e)) return ctypeTy;
	return typeTy;
}

Expression typeOfVectorTy(Expression e,Expression num)in{
	assert(isType(e)||isQNumeric(e));
	assert(num&&isSubtype(num.type,ℕt(true)));
}do{
	if(isQNumeric(e)) return qnumericTy;
	auto nume=num.eval();
	if(isZero(nume)) return utypeTy;
	if(isEmpty(e)){
		if(isNonzero(nume)) return etypeTy;
		return utypeTy;
	}
	return e.type;
}

Expression typeOfStringTy(bool classical){ return classical?ctypeTy:typeTy; }

Expression typeOfProductTy(bool[] isConst,Id[] names,Expression dom,Expression cod,bool isSquare,bool isTuple,CaptureAnnotation captureAnnotation,Annotation annotation,bool isClassical){
	return isClassical?ctypeTy:typeTy;
}