X-Git-Url: http://nitlanguage.org

diff --git a/src/modelize/modelize_property.nit b/src/modelize/modelize_property.nit
index b6371f6..aadfb5c 100644
--- a/src/modelize/modelize_property.nit
+++ b/src/modelize/modelize_property.nit
@@ -17,10 +17,11 @@
 # Analysis and verification of property definitions to instantiate model element
 module modelize_property
 
-import modelize_class
+intrude import modelize_class
 private import annotation
 
 redef class ToolContext
+	# Run `AClassdef::build_property` on the classdefs of each module
 	var modelize_property_phase: Phase = new ModelizePropertyPhase(self, [modelize_class_phase])
 end
 
@@ -36,9 +37,47 @@ private class ModelizePropertyPhase
 end
 
 redef class ModelBuilder
-	# Register the npropdef associated to each mpropdef
-	# FIXME: why not refine the `MPropDef` class with a nullable attribute?
-	var mpropdef2npropdef: HashMap[MPropDef, APropdef] = new HashMap[MPropDef, APropdef]
+	# Registration of the npropdef associated to each mpropdef.
+	#
+	# Public clients need to use `mpropdef2node` to access stuff.
+	private var mpropdef2npropdef = new HashMap[MPropDef, APropdef]
+
+	# Retrieve the associated AST node of a mpropertydef.
+	# This method is used to associate model entity with syntactic entities.
+	#
+	# If the property definition is not associated with a node, returns `null`.
+	fun mpropdef2node(mpropdef: MPropDef): nullable ANode
+	do
+		var res
+		res = mpropdef2npropdef.get_or_null(mpropdef)
+		if res != null then
+			# Run the phases on it
+			toolcontext.run_phases_on_npropdef(res)
+			return res
+		end
+		if mpropdef isa MMethodDef and mpropdef.mproperty.is_root_init then
+			res = mclassdef2nclassdef.get_or_null(mpropdef.mclassdef)
+			if res != null then return res
+		end
+		return null
+	end
+
+	# Retrieve all the attributes nodes localy definied
+	# FIXME think more about this method and how the separations separate/global and ast/model should be done.
+	fun collect_attr_propdef(mclassdef: MClassDef): Array[AAttrPropdef]
+	do
+		var res = new Array[AAttrPropdef]
+		var n = mclassdef2nclassdef.get_or_null(mclassdef)
+		if n == null then return res
+		for npropdef in n.n_propdefs do
+			if npropdef isa AAttrPropdef then
+				# Run the phases on it
+				toolcontext.run_phases_on_npropdef(npropdef)
+				res.add(npropdef)
+			end
+		end
+		return res
+	end
 
 	# Build the properties of `nclassdef`.
 	# REQUIRE: all superclasses are built.
@@ -47,13 +86,15 @@ redef class ModelBuilder
 		# Force building recursively
 		if nclassdef.build_properties_is_done then return
 		nclassdef.build_properties_is_done = true
-		var mclassdef = nclassdef.mclassdef.as(not null)
+		var mclassdef = nclassdef.mclassdef
+		if mclassdef == null then return # skip error
 		if mclassdef.in_hierarchy == null then return # Skip error
 		for superclassdef in mclassdef.in_hierarchy.direct_greaters do
 			if not mclassdef2nclassdef.has_key(superclassdef) then continue
 			build_properties(mclassdef2nclassdef[superclassdef])
 		end
 
+		mclassdef.build_self_type(self, nclassdef)
 		for nclassdef2 in nclassdef.all_defs do
 			for npropdef in nclassdef2.n_propdefs do
 				npropdef.build_property(self, mclassdef)
@@ -62,6 +103,25 @@ redef class ModelBuilder
 				npropdef.build_signature(self)
 			end
 			for npropdef in nclassdef2.n_propdefs do
+				if not npropdef isa ATypePropdef then continue
+				# Check circularity
+				var mpropdef = npropdef.mpropdef
+				if mpropdef == null then continue
+				if mpropdef.bound == null then continue
+				if not check_virtual_types_circularity(npropdef, mpropdef.mproperty, mclassdef.bound_mtype, mclassdef.mmodule) then
+					# Invalidate the bound
+					mpropdef.is_broken = true
+					mpropdef.bound = mclassdef.mmodule.model.null_type
+				end
+			end
+			for npropdef in nclassdef2.n_propdefs do
+				# Check ATypePropdef first since they may be required for the other properties
+				if not npropdef isa ATypePropdef then continue
+				npropdef.check_signature(self)
+			end
+
+			for npropdef in nclassdef2.n_propdefs do
+				if npropdef isa ATypePropdef then continue
 				npropdef.check_signature(self)
 			end
 		end
@@ -82,8 +142,6 @@ redef class ModelBuilder
 		# Are we a refinement
 		if not mclassdef.is_intro then return
 
-		var mmodule = nclassdef.mclassdef.mmodule
-
 		# Look for the init in Object, or create it
 		if mclassdef.mclass.name == "Object" and the_root_init_mmethod == null then
 			# Create the implicit root-init method
@@ -101,9 +159,6 @@ redef class ModelBuilder
 			return
 		end
 
-		# Is the class forbid constructors?
-		if not mclassdef.mclass.kind.need_init then return
-
 		# Is there already a constructor defined?
 		var defined_init: nullable MMethodDef = null
 		for mpropdef in mclassdef.mpropdefs do
@@ -112,150 +167,175 @@ redef class ModelBuilder
 			if mpropdef.mproperty.is_root_init then
 				assert defined_init == null
 				defined_init = mpropdef
-			else
-				# An explicit old-style init, so return
+			else if mpropdef.mproperty.name == "init" then
+				# An explicit old-style init named "init", so return
 				return
 			end
 		end
 
 		if not nclassdef isa AStdClassdef then return
 
-		# Do we inherit a old-style constructor?
-		var combine = new Array[MMethod] # old-style constructors without arguments
-		var inhc: nullable MClass = null # single super-class with a constructor with arguments
-		if defined_init == null then for st in mclassdef.supertypes do
-			var c = st.mclass
-			if not c.kind.need_init then continue
-			st = st.anchor_to(mmodule, mclassdef.bound_mtype)
-			var candidate = self.try_get_mproperty_by_name2(nclassdef, mmodule, st, "init").as(nullable MMethod)
-			if candidate != null then
-				if candidate.is_root_init then continue
-				if candidate.intro.msignature != null then
-					if candidate.intro.msignature.arity == 0 then
-						combine.add(candidate)
-						continue
-					end
-				end
-			end
-			var inhc2 = c.inherit_init_from
-			if inhc2 == null then inhc2 = c
-			if inhc2 == inhc then continue
-			if inhc != null then
-				self.error(nclassdef, "Error: Cannot provide a defaut constructor: conflict for {inhc} and {c}")
-			else
-				inhc = inhc2
-			end
-		end
-
 		# Collect undefined attributes
 		var mparameters = new Array[MParameter]
 		var initializers = new Array[MProperty]
-		var anode: nullable ANode = null
 		for npropdef in nclassdef.n_propdefs do
+			if npropdef isa AMethPropdef then
+				if not npropdef.is_autoinit then continue # Skip non tagged autoinit
+				if npropdef.mpropdef == null then return # Skip broken method
+				var sig = npropdef.mpropdef.msignature
+				if sig == null then continue # Skip broken method
+
+				for param in sig.mparameters do
+					var ret_type = param.mtype
+					var mparameter = new MParameter(param.name, ret_type, false)
+					mparameters.add(mparameter)
+				end
+				initializers.add(npropdef.mpropdef.mproperty)
+				npropdef.mpropdef.mproperty.is_autoinit = true
+			end
 			if npropdef isa AAttrPropdef then
-				if npropdef.mpropdef == null then return # Skip broken attribute
-				var at = npropdef.get_single_annotation("noinit", self)
-				if at != null then
-					npropdef.noinit = true
-					if npropdef.n_expr != null then
-						self.error(at, "Error: `noinit` attributes cannot have an initial value")
-					end
-					continue # Skip noinit attributes
+				var mreadpropdef = npropdef.mreadpropdef
+				if mreadpropdef == null or mreadpropdef.msignature == null then return # Skip broken attribute
+				if npropdef.noinit then continue # Skip noinit attribute
+				var atlateinit = npropdef.get_single_annotation("lateinit", self)
+				if atlateinit != null then
+					# For lateinit attributes, call the reader to force
+					# the lazy initialization of the attribute.
+					initializers.add(mreadpropdef.mproperty)
+					mreadpropdef.mproperty.is_autoinit = true
+					continue
 				end
-				if npropdef.n_expr != null then continue
-				var paramname = npropdef.mpropdef.mproperty.name.substring_from(1)
-				var ret_type = npropdef.mpropdef.static_mtype
+				if npropdef.has_value then continue
+				var paramname = mreadpropdef.mproperty.name
+				var ret_type = mreadpropdef.msignature.return_mtype
 				if ret_type == null then return
 				var mparameter = new MParameter(paramname, ret_type, false)
 				mparameters.add(mparameter)
 				var msetter = npropdef.mwritepropdef
 				if msetter == null then
-					# No setter, it is a old-style attribute, so just add it
+					# No setter, it is a readonly attribute, so just add it
 					initializers.add(npropdef.mpropdef.mproperty)
+					npropdef.mpropdef.mproperty.is_autoinit = true
 				else
 					# Add the setter to the list
 					initializers.add(msetter.mproperty)
+					msetter.mproperty.is_autoinit = true
 				end
-				if anode == null then anode = npropdef
 			end
 		end
-		if anode == null then anode = nclassdef
 
-		if combine.is_empty and inhc != null then
-			if not mparameters.is_empty then
-				self.error(anode,"Error: {mclassdef} cannot inherit constructors from {inhc} because there is attributes without initial values: {mparameters.join(", ")}")
-				return
-			end
-
-			# TODO: actively inherit the consturctor
-			self.toolcontext.info("{mclassdef} inherits all constructors from {inhc}", 3)
-			#mclassdef.mclass.inherit_init_from = inhc
-			#return
-		end
+		if the_root_init_mmethod == null then return
 
-		if not combine.is_empty and inhc != null then
-			self.error(nclassdef, "Error: Cannot provide a defaut constructor: conflict for {combine.join(", ")} and {inhc}")
+		# Look for most-specific new-stype init definitions
+		var spropdefs = the_root_init_mmethod.lookup_super_definitions(mclassdef.mmodule, mclassdef.bound_mtype)
+		if spropdefs.is_empty then
+			toolcontext.error(nclassdef.location, "Error: `{mclassdef}` does not specialize `{the_root_init_mmethod.intro_mclassdef}`. Possible duplication of the root class `Object`?")
 			return
 		end
-		if not combine.is_empty then
-			if mparameters.is_empty and combine.length == 1 then
-				# No need to create a local init, the inherited one is enough
-				inhc = combine.first.intro_mclassdef.mclass
-				mclassdef.mclass.inherit_init_from = inhc
-				self.toolcontext.info("{mclassdef} inherits all constructors from {inhc}", 3)
-				return
+
+		# Look at the autoinit class-annotation
+		var autoinit = nclassdef.get_single_annotation("autoinit", self)
+		var noautoinit = nclassdef.get_single_annotation("noautoinit", self)
+		if autoinit != null then
+			# Just throws the collected initializers
+			mparameters.clear
+			initializers.clear
+
+			if noautoinit != null then
+				error(autoinit, "Error: `autoinit` and `noautoinit` are incompatible.")
 			end
-			nclassdef.super_inits = combine
-			var mprop = new MMethod(mclassdef, "init", mclassdef.mclass.visibility)
-			var mpropdef = new MMethodDef(mclassdef, mprop, nclassdef.location)
-			var msignature = new MSignature(mparameters, null)
-			mpropdef.msignature = msignature
-			mprop.is_init = true
-			nclassdef.mfree_init = mpropdef
-			self.toolcontext.info("{mclassdef} gets a free empty constructor {mpropdef}{msignature}", 3)
-			return
-		end
 
-		if the_root_init_mmethod == null then return
+			if autoinit.n_args.is_empty then
+				error(autoinit, "Syntax Error: `autoinit` expects method identifiers, use `noautoinit` to clear all autoinits.")
+			end
 
-		# Look for nost-specific new-stype init definitions
-		var spropdefs = the_root_init_mmethod.lookup_super_definitions(mclassdef.mmodule, mclassdef.bound_mtype)
-		if spropdefs.is_empty then
-			toolcontext.fatal_error(nclassdef.location, "Fatal error: {mclassdef} does not specialize {the_root_init_mmethod.intro_mclassdef}. Possible duplication of the root class `Object`?")
-		end
-
-		# Search the longest-one and checks for conflict
-		var longest = spropdefs.first
-		if spropdefs.length > 1 then
-			# Check for conflict in the order of initializers
-			# Each initializer list must me a prefix of the longest list
-			# part 1. find the longest list
-			for spd in spropdefs do
-				if spd.initializers.length > longest.initializers.length then longest = spd
-			end
-			# part 2. compare
-			for spd in spropdefs do
-				var i = 0
-				for p in spd.initializers do
-					if p != longest.initializers[i] then
-						self.error(nclassdef, "Error: conflict for inherited inits {spd}({spd.initializers.join(", ")}) and {longest}({longest.initializers.join(", ")})")
-						return
+			# Get and check each argument
+			for narg in autoinit.n_args do
+				var id = narg.as_id
+				if id == null then
+					error(narg, "Syntax Error: `autoinit` expects method identifiers.")
+					return
+				end
+
+				# Search the property.
+				# To avoid bad surprises, try to get the setter first.
+				var p = try_get_mproperty_by_name(narg, mclassdef, id + "=")
+				if p == null then
+					p = try_get_mproperty_by_name(narg, mclassdef, id)
+				end
+				if p == null then
+					error(narg, "Error: unknown method `{id}`")
+					return
+				end
+				if not p.is_autoinit then
+					error(narg, "Error: `{p}` is not an autoinit method")
+					return
+				end
+
+				# Register the initializer and the parameters
+				initializers.add(p)
+				var pd = p.intro
+				if pd isa MMethodDef then
+					# Get the signature resolved for the current receiver
+					var sig = pd.msignature.resolve_for(mclassdef.mclass.mclass_type, mclassdef.bound_mtype, mclassdef.mmodule, false)
+					mparameters.add_all(sig.mparameters)
+				else
+					# TODO attributes?
+					abort
+				end
+			end
+		else
+			# Search the longest-one and checks for conflict
+			var longest = spropdefs.first
+			if spropdefs.length > 1 then
+				# part 1. find the longest list
+				for spd in spropdefs do
+					if spd.initializers.length > longest.initializers.length then longest = spd
+				end
+				# part 2. compare
+				# Check for conflict in the order of initializers
+				# Each initializer list must me a prefix of the longest list
+				# If `noautoinit` is set, just ignore conflicts
+				if noautoinit == null then for spd in spropdefs do
+					var i = 0
+					for p in spd.initializers do
+						if p != longest.initializers[i] then
+							var proposal = new ArraySet[MProperty]
+							for spd2 in spropdefs do
+								proposal.add_all spd2.initializers
+							end
+							proposal.add_all initializers
+							self.error(nclassdef, "Error: cannot generate automatic init for class {mclassdef.mclass}. Conflict in the order in inherited initializers {spd}({spd.initializers.join(", ")}) and {longest}({longest.initializers.join(", ")}). Use `autoinit` to order initializers. eg `autoinit {proposal.join(", ")}`")
+							# TODO: invalidate the initializer to avoid more errors
+							return
+						end
+						i += 1
 					end
-					i += 1
 				end
 			end
-		end
 
-		# Can we just inherit?
-		if spropdefs.length == 1 and mparameters.is_empty and defined_init == null then
-			self.toolcontext.info("{mclassdef} inherits the basic constructor {longest}", 3)
-			return
-		end
+			if noautoinit != null then
+				# If there is local or inherited initializers, then complain.
+				if initializers.is_empty and longest.initializers.is_empty then
+					warning(noautoinit, "useless-noautoinit", "Warning: the list of autoinit is already empty.")
+				end
+				# Just clear initializers
+				mparameters.clear
+				initializers.clear
+			else
+				# Can we just inherit?
+				if spropdefs.length == 1 and mparameters.is_empty and defined_init == null then
+					self.toolcontext.info("{mclassdef} inherits the basic constructor {longest}", 3)
+					mclassdef.mclass.root_init = longest
+					return
+				end
 
-		# Combine the inherited list to what is collected
-		if longest.initializers.length > 0 then
-			mparameters.prepend longest.new_msignature.mparameters
-			initializers.prepend longest.initializers
+				# Combine the inherited list to what is collected
+				if longest.initializers.length > 0 then
+					mparameters.prepend longest.new_msignature.mparameters
+					initializers.prepend longest.initializers
+				end
+			end
 		end
 
 		# If we already have a basic init definition, then setup its initializers
@@ -264,6 +344,7 @@ redef class ModelBuilder
 			var msignature = new MSignature(mparameters, null)
 			defined_init.new_msignature = msignature
 			self.toolcontext.info("{mclassdef} extends its basic constructor signature to {defined_init}{msignature}", 3)
+			mclassdef.mclass.root_init = defined_init
 			return
 		end
 
@@ -277,6 +358,7 @@ redef class ModelBuilder
 		mpropdef.msignature = new MSignature(new Array[MParameter], null) # always an empty real signature
 		nclassdef.mfree_init = mpropdef
 		self.toolcontext.info("{mclassdef} gets a free constructor for attributes {mpropdef}{msignature}", 3)
+		mclassdef.mclass.root_init = mpropdef
 	end
 
 	# Check the visibility of `mtype` as an element of the signature of `mpropdef`.
@@ -288,16 +370,18 @@ redef class ModelBuilder
 		# Extract visibility information of the main part of `mtype`
 		# It is a case-by case
 		var vis_type: nullable MVisibility = null # The own visibility of the type
-		var mmodule_type: nullable MModule = null # The origial module of the type
-		mtype = mtype.as_notnullable
+		var mmodule_type: nullable MModule = null # The original module of the type
+		mtype = mtype.undecorate
 		if mtype isa MClassType then
 			vis_type = mtype.mclass.visibility
-			mmodule_type = mtype.mclass.intro.mmodule
+			mmodule_type = mtype.mclass.intro_mmodule
 		else if mtype isa MVirtualType then
 			vis_type = mtype.mproperty.visibility
 			mmodule_type = mtype.mproperty.intro_mclassdef.mmodule
 		else if mtype isa MParameterType then
 			# nothing, always visible
+		else if mtype isa MNullType then
+			# nothing to do.
 		else
 			node.debug "Unexpected type {mtype}"
 			abort
@@ -307,10 +391,10 @@ redef class ModelBuilder
 			assert mmodule_type != null
 			var vis_module_type = mmodule.visibility_for(mmodule_type) # the visibility of the original module
 			if mproperty.visibility > vis_type then
-				error(node, "Error: The {mproperty.visibility} property `{mproperty}` cannot contain the {vis_type} type `{mtype}`")
+				error(node, "Error: the {mproperty.visibility} property `{mproperty}` cannot contain the {vis_type} type `{mtype}`.")
 				return
 			else if mproperty.visibility > vis_module_type then
-				error(node, "Error: The {mproperty.visibility} property `{mproperty}` cannot contain the type `{mtype}` from the {vis_module_type} module `{mmodule_type}`")
+				error(node, "Error: the {mproperty.visibility} property `{mproperty}` cannot contain the type `{mtype}` from the {vis_module_type} module `{mmodule_type}`.")
 				return
 			end
 		end
@@ -326,12 +410,72 @@ redef class ModelBuilder
 			for t in mtype.arguments do check_visibility(node, t, mpropdef)
 		end
 	end
-end
 
-redef class MClass
-	# The class whose self inherit all the constructors.
-	# FIXME: this is needed to implement the crazy constructor mixin thing of the of old compiler. We need to think what to do with since this cannot stay in the modelbuilder
-	var inherit_init_from: nullable MClass = null
+	# Detect circularity errors for virtual types.
+	fun check_virtual_types_circularity(node: ANode, mproperty: MVirtualTypeProp, recv: MType, mmodule: MModule): Bool
+	do
+		# Check circularity
+		# Slow case: progress on each resolution until we visit all without getting a loop
+
+		# The graph used to detect loops
+		var mtype = mproperty.mvirtualtype
+		var poset = new POSet[MType]
+
+		# The work-list of types to resolve
+		var todo = new List[MType]
+		todo.add mtype
+
+		while not todo.is_empty do
+			# The visited type
+			var t = todo.pop
+
+			if not t.need_anchor then continue
+
+			# Get the types derived of `t` (subtypes and bounds)
+			var nexts
+			if t isa MNullableType then
+				nexts = [t.mtype]
+			else if t isa MGenericType then
+				nexts = t.arguments
+			else if t isa MVirtualType then
+				var vt = t.mproperty
+				# Because `vt` is possibly unchecked, we have to do the bound-lookup manually
+				var defs = vt.lookup_definitions(mmodule, recv)
+				# TODO something to manage correctly bound conflicts
+				assert not defs.is_empty
+				nexts = new Array[MType]
+				for d in defs do
+					var next = defs.first.bound
+					if next == null then return false
+					nexts.add next
+				end
+			else if t isa MClassType then
+				# Basic type, nothing to to
+				continue
+			else if t isa MParameterType then
+				# Parameter types cannot depend on virtual types, so nothing to do
+				continue
+			else
+				abort
+			end
+
+			# For each one
+			for next in nexts do
+				if poset.has_edge(next, t) then
+					if mtype == next then
+						error(node, "Error: circularity of virtual type definition: {next} <-> {t}.")
+					else
+						error(node, "Error: circularity of virtual type definition: {mtype} -> {next} <-> {t}.")
+					end
+					return false
+				else
+					poset.add_edge(t, next)
+					todo.add next
+				end
+			end
+		end
+		return true
+	end
 end
 
 redef class MPropDef
@@ -341,40 +485,69 @@ redef class MPropDef
 end
 
 redef class AClassdef
-	var build_properties_is_done: Bool = false
-	# The list of super-constructor to call at the start of the free constructor
-	# FIXME: this is needed to implement the crazy constructor thing of the of old compiler. We need to think what to do with since this cannot stay in the modelbuilder
-	var super_inits: nullable Collection[MMethod] = null
+	# Marker used in `ModelBuilder::build_properties`
+	private var build_properties_is_done = false
 
 	# The free init (implicitely constructed by the class if required)
 	var mfree_init: nullable MMethodDef = null
 end
 
+redef class MClass
+	# The base init of the class.
+	# Used to get the common new_msignature and initializers
+	#
+	# TODO: Where to put this information is not clear because unlike other
+	# informations, the initialisers are stable in a same class.
+	var root_init: nullable MMethodDef = null
+end
+
 redef class MClassDef
 	# What is the `APropdef` associated to a `MProperty`?
 	# Used to check multiple definition of a property.
 	var mprop2npropdef: Map[MProperty, APropdef] = new HashMap[MProperty, APropdef]
-end
 
-redef class Prod
-	# Join the text of all tokens
-	# Used to get the 'real name' of method definitions.
-	fun collect_text: String
+	# Build the virtual type `SELF` only for introduction `MClassDef`
+	fun build_self_type(modelbuilder: ModelBuilder, nclassdef: AClassdef)
 	do
-		var v = new TextCollectorVisitor
-		v.enter_visit(self)
-		assert v.text != ""
-		return v.text
-	end
-end
+		if not is_intro then return
 
-private class TextCollectorVisitor
-	super Visitor
-	var text: String = ""
-	redef fun visit(n)
-	do
-		if n isa Token then text += n.text
-		n.visit_all(self)
+		var name = "SELF"
+		var mprop = modelbuilder.try_get_mproperty_by_name(nclassdef, self, name)
+
+		# If SELF type is declared nowherer?
+		if mprop == null then return
+
+		# SELF is not a virtual type? it is weird but we ignore it
+		if not mprop isa MVirtualTypeProp then return
+
+		# Is this the intro of SELF in the library?
+		var intro = mprop.intro
+		var intro_mclassdef = intro.mclassdef
+		if intro_mclassdef == self then
+			var nintro = modelbuilder.mpropdef2npropdef[intro]
+
+			# SELF must be declared in Object, otherwise this will create conflicts
+			if intro_mclassdef.mclass.name != "Object" then
+				modelbuilder.error(nintro, "Error: the virtual type `SELF` must be declared in `Object`.")
+			end
+
+			# SELF must be public
+			if mprop.visibility != public_visibility then
+				modelbuilder.error(nintro, "Error: the virtual type `SELF` must be public.")
+			end
+
+			# SELF must not be fixed
+			if intro.is_fixed then
+				modelbuilder.error(nintro, "Error: the virtual type `SELF` cannot be fixed.")
+			end
+
+			return
+		end
+
+		# This class introduction inherits a SELF
+		# We insert an artificial property to update it
+		var mpropdef = new MVirtualTypeDef(self, mprop, self.location)
+		mpropdef.bound = mclass.mclass_type
 	end
 end
 
@@ -385,27 +558,26 @@ redef class APropdef
 	# The associated propdef once build by a `ModelBuilder`
 	var mpropdef: nullable MPROPDEF is writable
 
-	private fun build_property(modelbuilder: ModelBuilder, mclassdef: MClassDef) is abstract
-	private fun build_signature(modelbuilder: ModelBuilder) is abstract
-	private fun check_signature(modelbuilder: ModelBuilder) is abstract
+	private fun build_property(modelbuilder: ModelBuilder, mclassdef: MClassDef) do end
+	private fun build_signature(modelbuilder: ModelBuilder) do end
+	private fun check_signature(modelbuilder: ModelBuilder) do end
 	private fun new_property_visibility(modelbuilder: ModelBuilder, mclassdef: MClassDef, nvisibility: nullable AVisibility): MVisibility
 	do
 		var mvisibility = public_visibility
 		if nvisibility != null then
 			mvisibility = nvisibility.mvisibility
 			if mvisibility == intrude_visibility then
-				modelbuilder.error(nvisibility, "Error: intrude is not a legal visibility for properties.")
+				modelbuilder.error(nvisibility, "Error: `intrude` is not a legal visibility for properties.")
 				mvisibility = public_visibility
 			end
 		end
 		if mclassdef.mclass.visibility == private_visibility then
 			if mvisibility == protected_visibility then
 				assert nvisibility != null
-				modelbuilder.error(nvisibility, "Error: The only legal visibility for properties in a private class is private.")
+				modelbuilder.error(nvisibility, "Error: `private` is the only legal visibility for properties in a private class.")
 			else if mvisibility == private_visibility then
 				assert nvisibility != null
-				# Not yet
-				modelbuilder.warning(nvisibility, "useless-visibility", "Warning: private is superfluous since the only legal visibility for properties in a private class is private.")
+				modelbuilder.advice(nvisibility, "useless-visibility", "Warning: `private` is superfluous since the only legal visibility for properties in a private class is private.")
 			end
 			mvisibility = private_visibility
 		end
@@ -419,6 +591,8 @@ redef class APropdef
 			var mdoc = ndoc.to_mdoc
 			mpropdef.mdoc = mdoc
 			mdoc.original_mentity = mpropdef
+		else if mpropdef.is_intro and mpropdef.mproperty.visibility >= protected_visibility then
+			modelbuilder.advice(self, "missing-doc", "Documentation warning: Undocumented property `{mpropdef.mproperty}`")
 		end
 
 		var at_deprecated = get_single_annotation("deprecated", modelbuilder)
@@ -439,39 +613,45 @@ redef class APropdef
 		if nvisibility == null then return
 		var mvisibility = nvisibility.mvisibility
 		if mvisibility != mprop.visibility and mvisibility != public_visibility then
-				modelbuilder.error(nvisibility, "Error: redefinition changed the visibility from a {mprop.visibility} to a {mvisibility}")
+				modelbuilder.error(nvisibility, "Error: redefinition changed the visibility from `{mprop.visibility}` to `{mvisibility}`.")
 		end
 	end
 
 	private fun check_redef_keyword(modelbuilder: ModelBuilder, mclassdef: MClassDef, kwredef: nullable Token, need_redef: Bool, mprop: MProperty): Bool
 	do
 		if mclassdef.mprop2npropdef.has_key(mprop) then
-			modelbuilder.error(self, "Error: A property {mprop} is already defined in class {mclassdef.mclass} at line {mclassdef.mprop2npropdef[mprop].location.line_start}.")
-			return false
-		end
-		if mprop isa MMethod and mprop.is_toplevel != (parent isa ATopClassdef) then
-			if mprop.is_toplevel then
-				modelbuilder.error(self, "Error: {mprop} is a top level method.")
-			else
-				modelbuilder.error(self, "Error: {mprop} is not a top level method.")
-			end
+			modelbuilder.error(self, "Error: a property `{mprop}` is already defined in class `{mclassdef.mclass}` at line {mclassdef.mprop2npropdef[mprop].location.line_start}.")
 			return false
-
 		end
+		if mprop isa MMethod and mprop.is_root_init then return true
 		if kwredef == null then
 			if need_redef then
-				modelbuilder.error(self, "Redef error: {mclassdef.mclass}::{mprop.name} is an inherited property. To redefine it, add the redef keyword.")
+				modelbuilder.error(self, "Redef Error: `{mclassdef.mclass}::{mprop.name}` is an inherited property. To redefine it, add the `redef` keyword.")
 				return false
 			end
+
+			# Check for full-name conflicts in the package.
+			# A public property should have a unique qualified name `package::class::prop`.
+			if mprop.intro_mclassdef.mmodule.mgroup != null and mprop.visibility >= protected_visibility then
+				var others = modelbuilder.model.get_mproperties_by_name(mprop.name)
+				if others != null then for other in others do
+					if other != mprop and other.intro_mclassdef.mmodule.mgroup != null and other.intro_mclassdef.mmodule.mgroup.mpackage == mprop.intro_mclassdef.mmodule.mgroup.mpackage and other.intro_mclassdef.mclass.name == mprop.intro_mclassdef.mclass.name and other.visibility >= protected_visibility then
+						modelbuilder.advice(self, "full-name-conflict", "Warning: A property named `{other.full_name}` is already defined in module `{other.intro_mclassdef.mmodule}` for the class `{other.intro_mclassdef.mclass.name}`.")
+						break
+					end
+				end
+			end
 		else
 			if not need_redef then
-				modelbuilder.error(self, "Error: No property {mclassdef.mclass}::{mprop.name} is inherited. Remove the redef keyword to define a new property.")
+				modelbuilder.error(self, "Error: no property `{mclassdef.mclass}::{mprop.name}` is inherited. Remove the `redef` keyword to define a new property.")
 				return false
 			end
 		end
 		return true
 	end
 
+	# Checks for useless type in redef signatures.
+	private fun check_repeated_types(modelbuilder: ModelBuilder) do end
 end
 
 redef class ASignature
@@ -499,14 +679,14 @@ redef class ASignature
 			param_names.add(np.n_id.text)
 			var ntype = np.n_type
 			if ntype != null then
-				var mtype = modelbuilder.resolve_mtype(mmodule, mclassdef, ntype)
+				var mtype = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, ntype, true)
 				if mtype == null then return false # Skip error
 				for i in [0..param_names.length-param_types.length[ do
 					param_types.add(mtype)
 				end
 				if np.n_dotdotdot != null then
 					if self.vararg_rank != -1 then
-						modelbuilder.error(np, "Error: {param_names[self.vararg_rank]} is already a vararg")
+						modelbuilder.error(np, "Error: `{param_names[self.vararg_rank]}` is already a vararg")
 						return false
 					else
 						self.vararg_rank = param_names.length - 1
@@ -516,32 +696,33 @@ redef class ASignature
 		end
 		var ntype = self.n_type
 		if ntype != null then
-			self.ret_type = modelbuilder.resolve_mtype(mmodule, mclassdef, ntype)
-			if self.ret_type == null then return false # Skip errir
+			self.ret_type = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, ntype, true)
+			if self.ret_type == null then return false # Skip error
 		end
 
 		self.is_visited = true
 		return true
 	end
 
-	# Build a visited signature
-	fun build_signature(modelbuilder: ModelBuilder): nullable MSignature
+	private fun check_signature(modelbuilder: ModelBuilder, mclassdef: MClassDef): Bool
 	do
-		if param_names.length != param_types.length then
-			# Some parameters are typed, other parameters are not typed.
-			modelbuilder.error(self.n_params[param_types.length], "Error: Untyped parameter `{param_names[param_types.length]}'.")
-			return null
+		var res = true
+		for np in self.n_params do
+			var ntype = np.n_type
+			if ntype != null then
+				if modelbuilder.resolve_mtype(mclassdef.mmodule, mclassdef, ntype) == null then
+					res = false
+				end
+			end
 		end
-
-		var mparameters = new Array[MParameter]
-		for i in [0..param_names.length[ do
-			var mparameter = new MParameter(param_names[i], param_types[i], i == vararg_rank)
-			self.n_params[i].mparameter = mparameter
-			mparameters.add(mparameter)
+		var ntype = self.n_type
+		if ntype != null then
+			if modelbuilder.resolve_mtype(mclassdef.mmodule, mclassdef, ntype) == null then
+				res = false
+			end
 		end
-
-		var msignature = new MSignature(mparameters, ret_type)
-		return msignature
+		if not res then is_broken = true
+		return res
 	end
 end
 
@@ -553,18 +734,16 @@ end
 redef class AMethPropdef
 	redef type MPROPDEF: MMethodDef
 
+	# Is the method annotated `autoinit`?
+	var is_autoinit = false
 
 	# Can self be used as a root init?
-	private fun look_like_a_root_init(modelbuilder: ModelBuilder): Bool
+	private fun look_like_a_root_init(modelbuilder: ModelBuilder, mclassdef: MClassDef): Bool
 	do
 		# Need the `init` keyword
 		if n_kwinit == null then return false
 		# Need to by anonymous
 		if self.n_methid != null then return false
-		# No parameters
-		if self.n_signature.n_params.length > 0 then return false
-		# Cannot be private or something
-		if not self.n_visibility isa APublicVisibility then return false
 		# No annotation on itself
 		if get_single_annotation("old_style_init", modelbuilder) != null then return false
 		# Nor on its module
@@ -574,6 +753,16 @@ redef class AMethPropdef
 			var old = amoddecl.get_single_annotation("old_style_init", modelbuilder)
 			if old != null then return false
 		end
+		# No parameters
+		if self.n_signature.n_params.length > 0 then
+			modelbuilder.advice(self, "old-init", "Warning: init with signature in {mclassdef}")
+			return false
+		end
+		# Cannot be private or something
+		if not self.n_visibility isa APublicVisibility then
+			modelbuilder.advice(self, "old-init", "Warning: non-public init in {mclassdef}")
+			return false
+		end
 
 		return true
 	end
@@ -594,7 +783,7 @@ redef class AMethPropdef
 				name = "init"
 				name_node = n_kwinit
 			else if n_kwnew != null then
-				name = "init"
+				name = "new"
 				name_node = n_kwnew
 			else
 				abort
@@ -607,31 +796,68 @@ redef class AMethPropdef
 			name = amethodid.collect_text
 			name_node = amethodid
 
-			if name == "-" and self.n_signature.n_params.length == 0 then
+			var arity = self.n_signature.n_params.length
+			if name == "+" and arity == 0 then
+				name = "unary +"
+			else if name == "-" and arity == 0 then
 				name = "unary -"
+			else if name == "~" and arity == 0 then
+				name = "unary ~"
+			else
+				if amethodid.is_binary and arity != 1 then
+					modelbuilder.error(self.n_signature, "Syntax Error: binary operator `{name}` requires exactly one parameter; got {arity}.")
+				else if amethodid.min_arity > arity then
+					modelbuilder.error(self.n_signature, "Syntax Error: `{name}` requires at least {amethodid.min_arity} parameter(s); got {arity}.")
+				end
 			end
 		end
 
+		var look_like_a_root_init = look_like_a_root_init(modelbuilder, mclassdef)
 		var mprop: nullable MMethod = null
 		if not is_init or n_kwredef != null then mprop = modelbuilder.try_get_mproperty_by_name(name_node, mclassdef, name).as(nullable MMethod)
-		if mprop == null and look_like_a_root_init(modelbuilder) then
+		if mprop == null and look_like_a_root_init then
 			mprop = modelbuilder.the_root_init_mmethod
+			var nb = n_block
+			if nb isa ABlockExpr and nb.n_expr.is_empty and n_doc == null then
+				modelbuilder.advice(self, "useless-init", "Warning: useless empty init in {mclassdef}")
+			end
 		end
 		if mprop == null then
 			var mvisibility = new_property_visibility(modelbuilder, mclassdef, self.n_visibility)
 			mprop = new MMethod(mclassdef, name, mvisibility)
-			if look_like_a_root_init(modelbuilder) and modelbuilder.the_root_init_mmethod == null then
+			if look_like_a_root_init and modelbuilder.the_root_init_mmethod == null then
 				modelbuilder.the_root_init_mmethod = mprop
 				mprop.is_root_init = true
 			end
 			mprop.is_init = is_init
 			mprop.is_new = n_kwnew != null
-			if parent isa ATopClassdef then mprop.is_toplevel = true
-			if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, false, mprop) then return
+			if mprop.is_new then mclassdef.mclass.has_new_factory = true
+			if name == "sys" then mprop.is_toplevel = true # special case for sys allowed in `new` factories
+			if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, false, mprop) then
+				mprop.is_broken = true
+				return
+			end
 		else
-			if not mprop.is_root_init and not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, not self isa AMainMethPropdef, mprop) then return
+			if mprop.is_broken then
+				return
+			end
+			if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, not self isa AMainMethPropdef, mprop) then return
 			check_redef_property_visibility(modelbuilder, self.n_visibility, mprop)
 		end
+
+		# Check name conflicts in the local class for constructors.
+		if is_init then
+			for p, n in mclassdef.mprop2npropdef do
+				if p != mprop and p isa MMethod and p.name == name then
+					if not check_redef_keyword(modelbuilder, mclassdef, n_kwredef, false, p) then
+						mprop.is_broken = true
+						return
+					end
+					break
+				end
+			end
+		end
+
 		mclassdef.mprop2npropdef[mprop] = self
 
 		var mpropdef = new MMethodDef(mclassdef, mprop, self.location)
@@ -641,9 +867,9 @@ redef class AMethPropdef
 		self.mpropdef = mpropdef
 		modelbuilder.mpropdef2npropdef[mpropdef] = self
 		if mpropdef.is_intro then
-			modelbuilder.toolcontext.info("{mpropdef} introduces new method {mprop.full_name}", 3)
+			modelbuilder.toolcontext.info("{mpropdef} introduces new method {mprop.full_name}", 4)
 		else
-			modelbuilder.toolcontext.info("{mpropdef} redefines method {mprop.full_name}", 3)
+			modelbuilder.toolcontext.info("{mpropdef} redefines method {mprop.full_name}", 4)
 		end
 	end
 
@@ -655,6 +881,19 @@ redef class AMethPropdef
 		var mmodule = mclassdef.mmodule
 		var nsig = self.n_signature
 
+		if mpropdef.mproperty.is_root_init and not mclassdef.is_intro then
+			var root_init = mclassdef.mclass.root_init
+			if root_init != null then
+				# Inherit the initializers by refinement
+				mpropdef.new_msignature = root_init.new_msignature
+				assert mpropdef.initializers.is_empty
+				mpropdef.initializers.add_all root_init.initializers
+			end
+		end
+
+		var accept_special_last_parameter = self.n_methid == null or self.n_methid.accept_special_last_parameter
+		var return_is_mandatory = self.n_methid != null and self.n_methid.return_is_mandatory
+
 		# Retrieve info from the signature AST
 		var param_names = new Array[String] # Names of parameters from the AST
 		var param_types = new Array[MType] # Types of parameters from the AST
@@ -675,14 +914,17 @@ redef class AMethPropdef
 			msignature = mpropdef.mproperty.intro.msignature
 			if msignature == null then return # Skip error
 
+			# The local signature is adapted to use the local formal types, if any.
+			msignature = msignature.resolve_for(mclassdef.mclass.mclass_type, mclassdef.bound_mtype, mmodule, false)
+
 			# Check inherited signature arity
 			if param_names.length != msignature.arity then
 				var node: ANode
 				if nsig != null then node = nsig else node = self
-				modelbuilder.error(node, "Redef error: {mpropdef} redefines {mpropdef.mproperty.intro} with {param_names.length} parameter(s), {msignature.arity} expected. Signature is {mpropdef}{msignature}")
+				modelbuilder.error(node, "Redef Error: expected {msignature.arity} parameter(s) for `{mpropdef.mproperty.name}{msignature}`; got {param_names.length}. See introduction at `{mpropdef.mproperty.full_name}`.")
 				return
 			end
-		else if mpropdef.mproperty.is_init then
+		else if mpropdef.mproperty.is_init and not mpropdef.mproperty.is_new then
 			# FIXME UGLY: inherit signature from a super-constructor
 			for msupertype in mclassdef.supertypes do
 				msupertype = msupertype.anchor_to(mmodule, mclassdef.bound_mtype)
@@ -711,7 +953,7 @@ redef class AMethPropdef
 
 		if param_names.length != param_types.length then
 			# Some parameters are typed, other parameters are not typed.
-			modelbuilder.error(nsig.n_params[param_types.length], "Error: Untyped parameter `{param_names[param_types.length]}'.")
+			modelbuilder.error(nsig.n_params[param_types.length], "Error: untyped parameter `{param_names[param_types.length]}'.")
 			return
 		end
 
@@ -722,11 +964,37 @@ redef class AMethPropdef
 			mparameters.add(mparameter)
 		end
 
+		# In `new`-factories, the return type is by default the classtype.
+		if ret_type == null and mpropdef.mproperty.is_new then ret_type = mclassdef.mclass.mclass_type
+
+		# Special checks for operator methods
+		if not accept_special_last_parameter and mparameters.not_empty and mparameters.last.is_vararg then
+			modelbuilder.error(self.n_signature.n_params.last, "Error: illegal variadic parameter `{mparameters.last}` for `{mpropdef.mproperty.name}`.")
+		end
+		if ret_type == null and return_is_mandatory then
+			modelbuilder.error(self.n_methid, "Error: mandatory return type for `{mpropdef.mproperty.name}`.")
+		end
+
 		msignature = new MSignature(mparameters, ret_type)
 		mpropdef.msignature = msignature
-		mpropdef.is_abstract = self isa ADeferredMethPropdef or self.get_single_annotation("abstract", modelbuilder) != null
-		mpropdef.is_intern = self isa AInternMethPropdef or self.get_single_annotation("intern", modelbuilder) != null
-		mpropdef.is_extern = self isa AExternPropdef or self.n_extern_code_block != null or self.get_single_annotation("extern", modelbuilder) != null
+		mpropdef.is_abstract = self.get_single_annotation("abstract", modelbuilder) != null
+		mpropdef.is_intern = self.get_single_annotation("intern", modelbuilder) != null
+		mpropdef.is_extern = self.n_extern_code_block != null or self.get_single_annotation("extern", modelbuilder) != null
+
+		# Check annotations
+		var at = self.get_single_annotation("lazy", modelbuilder)
+		if at != null then modelbuilder.error(at, "Syntax Error: `lazy` must be used on attributes.")
+
+		var atautoinit = self.get_single_annotation("autoinit", modelbuilder)
+		if atautoinit != null then
+			if not mpropdef.is_intro then
+				modelbuilder.error(atautoinit, "Error: `autoinit` cannot be set on redefinitions.")
+			else if not mclassdef.is_intro then
+				modelbuilder.error(atautoinit, "Error: `autoinit` cannot be used in class refinements.")
+			else
+				self.is_autoinit = true
+			end
+		end
 	end
 
 	redef fun check_signature(modelbuilder)
@@ -736,9 +1004,18 @@ redef class AMethPropdef
 		var mclassdef = mpropdef.mclassdef
 		var mmodule = mclassdef.mmodule
 		var nsig = self.n_signature
-		var mysignature = self.mpropdef.msignature
+		var mysignature = mpropdef.msignature
 		if mysignature == null then return # Error thus skiped
 
+		# Check
+		if nsig != null then
+			if not nsig.check_signature(modelbuilder, mclassdef) then
+				mpropdef.msignature = null # invalidate
+				mpropdef.is_broken = true
+				return # Forward error
+			end
+		end
+
 		# Lookup for signature in the precursor
 		# FIXME all precursors should be considered
 		if not mpropdef.is_intro then
@@ -748,7 +1025,9 @@ redef class AMethPropdef
 			var precursor_ret_type = msignature.return_mtype
 			var ret_type = mysignature.return_mtype
 			if ret_type != null and precursor_ret_type == null then
-				modelbuilder.error(nsig.n_type.as(not null), "Redef Error: {mpropdef.mproperty} is a procedure, not a function.")
+				modelbuilder.error(nsig.n_type.as(not null), "Redef Error: `{mpropdef.mproperty}` is a procedure, not a function.")
+				mpropdef.msignature = null
+				mpropdef.is_broken = true
 				return
 			end
 
@@ -757,18 +1036,25 @@ redef class AMethPropdef
 				for i in [0..mysignature.arity[ do
 					var myt = mysignature.mparameters[i].mtype
 					var prt = msignature.mparameters[i].mtype
-					if not myt.is_subtype(mmodule, mclassdef.bound_mtype, prt) or
-							not prt.is_subtype(mmodule, mclassdef.bound_mtype, myt) then
-						modelbuilder.error(nsig.n_params[i], "Redef Error: Wrong type for parameter `{mysignature.mparameters[i].name}'. found {myt}, expected {prt} as in {mpropdef.mproperty.intro}.")
+					var node = nsig.n_params[i]
+					if not modelbuilder.check_sametype(node, mmodule, mclassdef.bound_mtype, myt, prt) then
+						modelbuilder.error(node, "Redef Error: expected `{prt}` for parameter `{mysignature.mparameters[i].name}'; got `{myt}`.")
+						mpropdef.msignature = null
+						mpropdef.is_broken = true
 					end
 				end
 			end
 			if precursor_ret_type != null then
+				var node: nullable ANode = null
+				if nsig != null then node = nsig.n_type
+				if node == null then node = self
 				if ret_type == null then
 					# Inherit the return type
 					ret_type = precursor_ret_type
-				else if not ret_type.is_subtype(mmodule, mclassdef.bound_mtype, precursor_ret_type) then
-					modelbuilder.error(nsig.n_type.as(not null), "Redef Error: Wrong return type. found {ret_type}, expected {precursor_ret_type} as in {mpropdef.mproperty.intro}.")
+				else if not modelbuilder.check_subtype(node, mmodule, mclassdef.bound_mtype, ret_type, precursor_ret_type) then
+					modelbuilder.error(node, "Redef Error: expected `{precursor_ret_type}` for return type; got `{ret_type}`.")
+					mpropdef.msignature = null
+					mpropdef.is_broken = true
 				end
 			end
 		end
@@ -782,21 +1068,101 @@ redef class AMethPropdef
 			var nt = nsig.n_type
 			if nt != null then modelbuilder.check_visibility(nt, nt.mtype.as(not null), mpropdef)
 		end
+		check_repeated_types(modelbuilder)
+	end
+
+	# For parameters, type is always useless in a redef.
+	# For return type, type is useless if not covariant with introduction.
+	redef fun check_repeated_types(modelbuilder) do
+		if mpropdef.is_intro or n_signature == null then return
+		# check params
+		for param in n_signature.n_params do
+			if param.n_type != null then
+				modelbuilder.advice(param.n_type, "useless-signature", "Warning: useless type repetition on parameter `{param.n_id.text}` for redefined method `{mpropdef.name}`")
+			end
+		end
+		# get intro
+		var intro = mpropdef.mproperty.intro
+		var n_intro = modelbuilder.mpropdef2npropdef.get_or_null(intro)
+		if n_intro == null or not n_intro isa AMethPropdef then return
+		# check return type
+		var ret_type = n_signature.ret_type
+		if ret_type != null and ret_type == n_intro.n_signature.ret_type then
+			modelbuilder.advice(n_signature.n_type, "useless-signature", "Warning: useless return type repetition for redefined method `{mpropdef.name}`")
+		end
 	end
 end
 
+redef class AMethid
+	# Is a return required?
+	#
+	# * True for operators and brackets.
+	# * False for id and assignment.
+	fun return_is_mandatory: Bool do return true
+
+	# Can the last parameter be special like a vararg?
+	#
+	# * False for operators: the last one is in fact the only one.
+	# * False for assignments: it is the right part of the assignment.
+	# * True for ids and brackets.
+	fun accept_special_last_parameter: Bool do return false
+
+	# The minimum required number of parameters.
+	#
+	# * 1 for binary operators
+	# * 1 for brackets
+	# * 1 for assignments
+	# * 2 for bracket assignments
+	# * 0 for ids
+	fun min_arity: Int do return 1
+
+	# Is the `self` a binary operator?
+	fun is_binary: Bool do return true
+end
+
+redef class AIdMethid
+	redef fun return_is_mandatory do return false
+	redef fun accept_special_last_parameter do return true
+	redef fun min_arity do return 0
+	redef fun is_binary do return false
+end
+
+redef class ABraMethid
+	redef fun accept_special_last_parameter do return true
+	redef fun is_binary do return false
+end
+
+redef class ABraassignMethid
+	redef fun return_is_mandatory do return false
+	redef fun min_arity do return 2
+	redef fun is_binary do return false
+end
+
+redef class AAssignMethid
+	redef fun return_is_mandatory do return false
+	redef fun is_binary do return false
+end
+
 redef class AAttrPropdef
 	redef type MPROPDEF: MAttributeDef
 
+	# The static type of the property (declared, inferred or inherited)
+	# This attribute is also used to check if the property was analyzed and is valid.
+	var mtype: nullable MType
+
 	# Is the node tagged `noinit`?
 	var noinit = false
 
-	# Is the node taggeg lazy?
+	# Is the node tagged lazy?
 	var is_lazy = false
 
-	# The guard associated to a lasy attribute.
+	# Has the node a default value?
+	# Could be through `n_expr` or `n_block`
+	var has_value = false
+
+	# The guard associated to a lazy attribute.
 	# Because some engines does not have a working `isset`,
-	# this additionnal attribute is used to guard the lazy initialization.
+	# this additional attribute is used to guard the lazy initialization.
 	# TODO: to remove once isset is correctly implemented
 	var mlazypropdef: nullable MAttributeDef
 
@@ -808,140 +1174,202 @@ redef class AAttrPropdef
 	redef fun build_property(modelbuilder, mclassdef)
 	do
 		var mclass = mclassdef.mclass
+		var nid2 = n_id2
+		var name = nid2.text
 
-		var name: String
-		if self.n_id != null then
-			name = self.n_id.text
-		else
-			name = self.n_id2.text
-		end
-
-		if mclass.kind == interface_kind or mclassdef.mclass.kind == enum_kind then
-			modelbuilder.error(self, "Error: Attempt to define attribute {name} in the interface {mclass}.")
-		else if mclass.kind == enum_kind then
-			modelbuilder.error(self, "Error: Attempt to define attribute {name} in the enum class {mclass}.")
-		else if mclass.kind == extern_kind then
-			modelbuilder.error(self, "Error: Attempt to define attribute {name} in the extern class {mclass}.")
-		end
+		var atabstract = self.get_single_annotation("abstract", modelbuilder)
+		if atabstract == null then
+			if not mclass.kind.need_init then
+				modelbuilder.error(self, "Error: attempt to define attribute `{name}` in the {mclass.kind} `{mclass}`.")
+			end
 
-		var nid = self.n_id
-		if nid != null then
-			# Old attribute style
-			modelbuilder.error(nid, "Error: old-style attribute no more supported")
-		else
-			# New attribute style
-			var nid2 = self.n_id2.as(not null)
 			var mprop = new MAttribute(mclassdef, "_" + name, private_visibility)
 			var mpropdef = new MAttributeDef(mclassdef, mprop, self.location)
 			self.mpropdef = mpropdef
 			modelbuilder.mpropdef2npropdef[mpropdef] = self
-			set_doc(mpropdef, modelbuilder)
-
-			var readname = name
-			var mreadprop = modelbuilder.try_get_mproperty_by_name(nid2, mclassdef, readname).as(nullable MMethod)
-			if mreadprop == null then
-				var mvisibility = new_property_visibility(modelbuilder, mclassdef, self.n_visibility)
-				mreadprop = new MMethod(mclassdef, readname, mvisibility)
-				if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, false, mreadprop) then return
-				mreadprop.deprecation = mprop.deprecation
-			else
-				if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, true, mreadprop) then return
-				check_redef_property_visibility(modelbuilder, self.n_visibility, mreadprop)
-			end
-			mclassdef.mprop2npropdef[mreadprop] = self
+		end
 
-			var mreadpropdef = new MMethodDef(mclassdef, mreadprop, self.location)
-			self.mreadpropdef = mreadpropdef
-			modelbuilder.mpropdef2npropdef[mreadpropdef] = self
-			mreadpropdef.mdoc = mpropdef.mdoc
+		var readname = name
+		var mreadprop = modelbuilder.try_get_mproperty_by_name(nid2, mclassdef, readname).as(nullable MMethod)
+		if mreadprop == null then
+			var mvisibility = new_property_visibility(modelbuilder, mclassdef, self.n_visibility)
+			mreadprop = new MMethod(mclassdef, readname, mvisibility)
+			if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, false, mreadprop) then return
+		else
+			if not self.check_redef_keyword(modelbuilder, mclassdef, n_kwredef, true, mreadprop) then return
+			check_redef_property_visibility(modelbuilder, self.n_visibility, mreadprop)
+		end
+		mclassdef.mprop2npropdef[mreadprop] = self
 
-			var atlazy = self.get_single_annotation("lazy", modelbuilder)
-			if atlazy != null then
-				if n_expr == null then
-					modelbuilder.error(atlazy, "Error: a lazy attribute needs a value")
-				end
-				is_lazy = true
-				var mlazyprop = new MAttribute(mclassdef, "lazy _" + name, none_visibility)
-				var mlazypropdef = new MAttributeDef(mclassdef, mlazyprop, self.location)
-				self.mlazypropdef = mlazypropdef
+		var mreadpropdef = new MMethodDef(mclassdef, mreadprop, self.location)
+		self.mreadpropdef = mreadpropdef
+		modelbuilder.mpropdef2npropdef[mreadpropdef] = self
+		set_doc(mreadpropdef, modelbuilder)
+		if mpropdef != null then mpropdef.mdoc = mreadpropdef.mdoc
+		if atabstract != null then mreadpropdef.is_abstract = true
+
+		has_value = n_expr != null or n_block != null
+
+		if atabstract != null and has_value then
+			modelbuilder.error(atabstract, "Error: `abstract` attributes cannot have an initial value.")
+			return
+		end
+
+		var atnoinit = self.get_single_annotation("noinit", modelbuilder)
+		if atnoinit == null then atnoinit = self.get_single_annotation("noautoinit", modelbuilder)
+		if atnoinit != null then
+			noinit = true
+			if has_value then
+				modelbuilder.error(atnoinit, "Error: `noautoinit` attributes cannot have an initial value.")
+				return
 			end
+			if atabstract != null then
+				modelbuilder.warning(atnoinit, "useless-noautoinit", "Warning: superfluous `noautoinit` on abstract attribute.")
+			end
+		end
 
-			var atreadonly = self.get_single_annotation("readonly", modelbuilder)
-			if atreadonly != null then
-				if n_expr == null then
-					modelbuilder.error(atreadonly, "Error: a readonly attribute needs a value")
+		var atlazy = self.get_single_annotation("lazy", modelbuilder)
+		var atlateinit = self.get_single_annotation("lateinit", modelbuilder)
+		if atlazy != null or atlateinit != null then
+			if atlazy != null and atlateinit != null then
+				modelbuilder.error(atlazy, "Error: `lazy` incompatible with `lateinit`.")
+				return
+			end
+			if not has_value then
+				if atlazy != null then
+					modelbuilder.error(atlazy, "Error: `lazy` attributes need a value.")
+				else if atlateinit != null then
+					modelbuilder.error(atlateinit, "Error: `lateinit` attributes need a value.")
 				end
-				# No setter, so just leave
+				has_value = true
 				return
 			end
+			is_lazy = true
+			var mlazyprop = new MAttribute(mclassdef, "lazy _" + name, none_visibility)
+			var mlazypropdef = new MAttributeDef(mclassdef, mlazyprop, self.location)
+			self.mlazypropdef = mlazypropdef
+		end
 
-			var writename = name + "="
-			var nwritable = self.n_writable
-			if nwritable != null then modelbuilder.error(nwritable, "Error: old-style setter no more supported")
-			var atwritable = self.get_single_annotation("writable", modelbuilder)
-			if atwritable != null then
-				if not atwritable.n_args.is_empty then
-					writename = atwritable.arg_as_id(modelbuilder) or else writename
-				end
+		var atreadonly = self.get_single_annotation("readonly", modelbuilder)
+		if atreadonly != null then
+			if not has_value then
+				modelbuilder.error(atreadonly, "Error: `readonly` attributes need a value.")
 			end
-			var mwriteprop = modelbuilder.try_get_mproperty_by_name(nid2, mclassdef, writename).as(nullable MMethod)
-			var nwkwredef: nullable Token = null
-			if atwritable != null then nwkwredef = atwritable.n_kwredef
-			if mwriteprop == null then
-				var mvisibility
-				if atwritable != null then
-					mvisibility = new_property_visibility(modelbuilder, mclassdef, atwritable.n_visibility)
-				else
-					mvisibility = private_visibility
-				end
-				mwriteprop = new MMethod(mclassdef, writename, mvisibility)
-				if not self.check_redef_keyword(modelbuilder, mclassdef, nwkwredef, false, mwriteprop) then return
-				mwriteprop.deprecation = mprop.deprecation
+			# No setter, so just leave
+			return
+		end
+
+		if not mclassdef.is_intro and not has_value and not noinit then
+			modelbuilder.advice(self, "attr-in-refinement", "Warning: attributes in refinement need a value or `noautoinit`.")
+		end
+
+		var writename = name + "="
+		var atwritable = self.get_single_annotation("writable", modelbuilder)
+		if atwritable != null then
+			if not atwritable.n_args.is_empty then
+				writename = atwritable.arg_as_id(modelbuilder) or else writename
+			end
+		end
+		var mwriteprop = modelbuilder.try_get_mproperty_by_name(nid2, mclassdef, writename).as(nullable MMethod)
+		var nwkwredef: nullable Token = null
+		if atwritable != null then nwkwredef = atwritable.n_kwredef
+		if mwriteprop == null then
+			var mvisibility
+			if atwritable != null then
+				mvisibility = new_property_visibility(modelbuilder, mclassdef, atwritable.n_visibility)
 			else
-				if not self.check_redef_keyword(modelbuilder, mclassdef, nwkwredef or else n_kwredef, true, mwriteprop) then return
-				if atwritable != null then
-					check_redef_property_visibility(modelbuilder, atwritable.n_visibility, mwriteprop)
-				end
+				mvisibility = mreadprop.visibility
+				# By default, use protected visibility at most
+				if mvisibility > protected_visibility then mvisibility = protected_visibility
 			end
-			mclassdef.mprop2npropdef[mwriteprop] = self
-
-			var mwritepropdef = new MMethodDef(mclassdef, mwriteprop, self.location)
-			self.mwritepropdef = mwritepropdef
-			modelbuilder.mpropdef2npropdef[mwritepropdef] = self
-			mwritepropdef.mdoc = mpropdef.mdoc
+			mwriteprop = new MMethod(mclassdef, writename, mvisibility)
+			if not self.check_redef_keyword(modelbuilder, mclassdef, nwkwredef, false, mwriteprop) then return
+			mwriteprop.deprecation = mreadprop.deprecation
+		else
+			if not self.check_redef_keyword(modelbuilder, mclassdef, nwkwredef or else n_kwredef, true, mwriteprop) then return
+			if atwritable != null then
+				check_redef_property_visibility(modelbuilder, atwritable.n_visibility, mwriteprop)
+			end
+		end
+		mclassdef.mprop2npropdef[mwriteprop] = self
+
+		var mwritepropdef = new MMethodDef(mclassdef, mwriteprop, self.location)
+		self.mwritepropdef = mwritepropdef
+		modelbuilder.mpropdef2npropdef[mwritepropdef] = self
+		mwritepropdef.mdoc = mreadpropdef.mdoc
+		if atabstract != null then mwritepropdef.is_abstract = true
+
+		var atautoinit = self.get_single_annotation("autoinit", modelbuilder)
+		if atautoinit != null then
+			if has_value then
+				modelbuilder.error(atautoinit, "Error: `autoinit` attributes cannot have an initial value.")
+			else if not mwritepropdef.is_intro then
+				modelbuilder.error(atautoinit, "Error: `autoinit` attributes cannot be set on redefinitions.")
+			else if not mclassdef.is_intro then
+				modelbuilder.error(atautoinit, "Error: `autoinit` attributes cannot be used in class refinements.")
+			else if atabstract == null then
+				modelbuilder.warning(atautoinit, "useless-autoinit", "Warning: superfluous `autoinit` on attribute.")
+			end
+		else if atabstract != null then
+			# By default, abstract attribute are not autoinit
+			noinit = true
 		end
 	end
 
 	redef fun build_signature(modelbuilder)
 	do
+		var mreadpropdef = self.mreadpropdef
 		var mpropdef = self.mpropdef
-		if mpropdef == null then return # Error thus skiped
-		var mclassdef = mpropdef.mclassdef
+		if mreadpropdef == null then return # Error thus skipped
+		var mclassdef = mreadpropdef.mclassdef
 		var mmodule = mclassdef.mmodule
 		var mtype: nullable MType = null
 
-		var mreadpropdef = self.mreadpropdef
 
 		var ntype = self.n_type
 		if ntype != null then
-			mtype = modelbuilder.resolve_mtype(mmodule, mclassdef, ntype)
+			mtype = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, ntype, true)
 			if mtype == null then return
 		end
 
-		# Inherit the type from the getter (usually an abstact getter)
-		if mtype == null and mreadpropdef != null and not mreadpropdef.is_intro then
+		var inherited_type: nullable MType = null
+		# Inherit the type from the getter (usually an abstract getter)
+		if not mreadpropdef.is_intro then
 			var msignature = mreadpropdef.mproperty.intro.msignature
-			if msignature == null then return # Error, thus skiped
-			mtype = msignature.return_mtype
+			if msignature == null then return # Error, thus skipped
+			inherited_type = msignature.return_mtype
+			if inherited_type != null then
+				# The inherited type is adapted to use the local formal types, if any.
+				inherited_type = inherited_type.resolve_for(mclassdef.mclass.mclass_type, mclassdef.bound_mtype, mmodule, false)
+				if mtype == null then mtype = inherited_type
+			end
 		end
 
 		var nexpr = self.n_expr
 		if mtype == null then
 			if nexpr != null then
 				if nexpr isa ANewExpr then
-					mtype = modelbuilder.resolve_mtype(mmodule, mclassdef, nexpr.n_type)
-				else if nexpr isa AIntExpr then
-					var cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Int")
+					mtype = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, nexpr.n_type, true)
+				else if nexpr isa AIntegerExpr then
+					var cla: nullable MClass = null
+					if nexpr.value isa Int then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Int")
+					else if nexpr.value isa Byte then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Byte")
+					else if nexpr.value isa Int8 then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Int8")
+					else if nexpr.value isa Int16 then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Int16")
+					else if nexpr.value isa UInt16 then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "UInt16")
+					else if nexpr.value isa Int32 then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Int32")
+					else if nexpr.value isa UInt32 then
+						cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "UInt32")
+					else
+						# Should not happen, and should be updated as new types are added
+						abort
+					end
 					if cla != null then mtype = cla.mclass_type
 				else if nexpr isa AFloatExpr then
 					var cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "Float")
@@ -959,28 +1387,32 @@ redef class AAttrPropdef
 					var cla = modelbuilder.try_get_mclass_by_name(nexpr, mmodule, "String")
 					if cla != null then mtype = cla.mclass_type
 				else
-					modelbuilder.error(self, "Error: Untyped attribute {mpropdef}. Implicit typing allowed only for literals and new.")
+					modelbuilder.error(self, "Error: untyped attribute `{mreadpropdef}`. Implicit typing allowed only for literals and new.")
 				end
 
 				if mtype == null then return
 			end
-		else if ntype != null then
+		else if ntype != null and inherited_type == mtype then
 			if nexpr isa ANewExpr then
-				var xmtype = modelbuilder.resolve_mtype(mmodule, mclassdef, nexpr.n_type)
-				if xmtype == mtype and modelbuilder.toolcontext.opt_warn.value >= 2 then
-					modelbuilder.warning(ntype, "useless-type", "Warning: useless type definition")
+				var xmtype = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, nexpr.n_type, true)
+				if xmtype == mtype then
+					modelbuilder.advice(ntype, "useless-type", "Warning: useless type definition")
 				end
 			end
 		end
 
 		if mtype == null then
-			modelbuilder.error(self, "Error: Untyped attribute {mpropdef}")
+			modelbuilder.error(self, "Error: untyped attribute `{mreadpropdef}`.")
 			return
 		end
 
-		mpropdef.static_mtype = mtype
+		self.mtype = mtype
+
+		if mpropdef != null then
+			mpropdef.static_mtype = mtype
+		end
 
-		if mreadpropdef != null then
+		do
 			var msignature = new MSignature(new Array[MParameter], mtype)
 			mreadpropdef.msignature = msignature
 		end
@@ -988,11 +1420,7 @@ redef class AAttrPropdef
 		var mwritepropdef = self.mwritepropdef
 		if mwritepropdef != null then
 			var name: String
-			if n_id != null then
-				name = n_id.text.substring_from(1)
-			else
-				name = n_id2.text
-			end
+			name = n_id2.text
 			var mparameter = new MParameter(name, mtype, false)
 			var msignature = new MSignature([mparameter], null)
 			mwritepropdef.msignature = msignature
@@ -1002,17 +1430,28 @@ redef class AAttrPropdef
 		if mlazypropdef != null then
 			mlazypropdef.static_mtype = modelbuilder.model.get_mclasses_by_name("Bool").first.mclass_type
 		end
+		check_repeated_types(modelbuilder)
 	end
 
 	redef fun check_signature(modelbuilder)
 	do
 		var mpropdef = self.mpropdef
-		if mpropdef == null then return # Error thus skiped
+		if mpropdef == null then return # Error thus skipped
+		var ntype = self.n_type
+		var mtype = self.mtype
+		if mtype == null then return # Error thus skipped
+
 		var mclassdef = mpropdef.mclassdef
 		var mmodule = mclassdef.mmodule
-		var ntype = self.n_type
-		var mtype = self.mpropdef.static_mtype
-		if mtype == null then return # Error thus skiped
+
+		# Check types
+		if ntype != null then
+			if modelbuilder.resolve_mtype(mmodule, mclassdef, ntype) == null then return
+		end
+		var nexpr = n_expr
+		if nexpr isa ANewExpr then
+			if modelbuilder.resolve_mtype(mmodule, mclassdef, nexpr.n_type) == null then return
+		end
 
 		# Lookup for signature in the precursor
 		# FIXME all precursors should be considered
@@ -1021,7 +1460,7 @@ redef class AAttrPropdef
 			if precursor_type == null then return
 
 			if mtype != precursor_type then
-				modelbuilder.error(ntype.as(not null), "Redef Error: Wrong static type. found {mtype}, expected {precursor_type}.")
+				modelbuilder.error(ntype.as(not null), "Redef Error: expected `{precursor_type}` type as a bound; got `{mtype}`.")
 				return
 			end
 		end
@@ -1060,7 +1499,7 @@ redef class AAttrPropdef
 			if mysignature.arity != msignature.arity then
 				var node: ANode
 				if nsig != null then node = nsig else node = self
-				modelbuilder.error(node, "Redef Error: {mysignature.arity} parameters found, {msignature.arity} expected. Signature is {mpropdef}{msignature}")
+				modelbuilder.error(node, "Redef Error: expected {msignature.arity} parameter(s) for `{mpropdef.mproperty.name}{msignature}`; got {mysignature.arity}. See introduction at `{mpropdef.mproperty.full_name}`.")
 				return
 			end
 			var precursor_ret_type = msignature.return_mtype
@@ -1068,7 +1507,7 @@ redef class AAttrPropdef
 			if ret_type != null and precursor_ret_type == null then
 				var node: ANode
 				if nsig != null then node = nsig else node = self
-				modelbuilder.error(node, "Redef Error: {mpropdef.mproperty} is a procedure, not a function.")
+				modelbuilder.error(node, "Redef Error: `{mpropdef.mproperty}` is a procedure, not a function.")
 				return
 			end
 
@@ -1077,26 +1516,44 @@ redef class AAttrPropdef
 				for i in [0..mysignature.arity[ do
 					var myt = mysignature.mparameters[i].mtype
 					var prt = msignature.mparameters[i].mtype
-					if not myt.is_subtype(mmodule, mclassdef.bound_mtype, prt) or
-							not prt.is_subtype(mmodule, mclassdef.bound_mtype, myt) then
-						var node: ANode
-						if nsig != null then node = nsig else node = self
-						modelbuilder.error(node, "Redef Error: Wrong type for parameter `{mysignature.mparameters[i].name}'. found {myt}, expected {prt}.")
+					var node: ANode
+					if nsig != null then node = nsig else node = self
+					if not modelbuilder.check_sametype(node, mmodule, mclassdef.bound_mtype, myt, prt) then
+						modelbuilder.error(node, "Redef Error: expected `{prt}` type for parameter `{mysignature.mparameters[i].name}'; got `{myt}`.")
 					end
 				end
 			end
 			if precursor_ret_type != null then
+				var node: ANode
+				if nsig != null then node = nsig else node = self
 				if ret_type == null then
 					# Inherit the return type
 					ret_type = precursor_ret_type
-				else if not ret_type.is_subtype(mmodule, mclassdef.bound_mtype, precursor_ret_type) then
-					var node: ANode
-					if nsig != null then node = nsig else node = self
-					modelbuilder.error(node, "Redef Error: Wrong return type. found {ret_type}, expected {precursor_ret_type}.")
+				else if not modelbuilder.check_subtype(node, mmodule, mclassdef.bound_mtype, ret_type, precursor_ret_type) then
+					modelbuilder.error(node, "Redef Error: expected `{precursor_ret_type}` return type; got `{ret_type}`.")
 				end
 			end
 		end
 	end
+
+	# Type is useless if the attribute type is the same thant the intro.
+	redef fun check_repeated_types(modelbuilder) do
+		if mreadpropdef.is_intro or n_type == null then return
+		# get intro
+		var intro = mreadpropdef.mproperty.intro
+		var n_intro = modelbuilder.mpropdef2npropdef.get_or_null(intro)
+		if n_intro == null then return
+		# get intro type
+		var ntype = null
+		if n_intro isa AMethPropdef then
+			ntype = n_intro.n_signature.ret_type
+		else if n_intro isa AAttrPropdef and n_intro.n_type != null then
+			ntype = n_intro.n_type.mtype
+		end
+		# check
+		if ntype ==null or ntype != n_type.mtype then return
+		modelbuilder.advice(n_type, "useless-signature", "Warning: useless type repetition on redefined attribute `{mpropdef.name}`")
+	end
 end
 
 redef class ATypePropdef
@@ -1110,7 +1567,7 @@ redef class ATypePropdef
 			var mvisibility = new_property_visibility(modelbuilder, mclassdef, self.n_visibility)
 			mprop = new MVirtualTypeProp(mclassdef, name, mvisibility)
 			for c in name.chars do if c >= 'a' and c<= 'z' then
-				modelbuilder.warning(n_id, "bad-type-name", "Warning: lowercase in the virtual type {name}")
+				modelbuilder.warning(n_id, "bad-type-name", "Warning: lowercase in the virtual type `{name}`.")
 				break
 			end
 			if not self.check_redef_keyword(modelbuilder, mclassdef, self.n_kwredef, false, mprop) then return
@@ -1124,6 +1581,11 @@ redef class ATypePropdef
 		var mpropdef = new MVirtualTypeDef(mclassdef, mprop, self.location)
 		self.mpropdef = mpropdef
 		modelbuilder.mpropdef2npropdef[mpropdef] = self
+		if mpropdef.is_intro then
+			modelbuilder.toolcontext.info("{mpropdef} introduces new type {mprop.full_name}", 4)
+		else
+			modelbuilder.toolcontext.info("{mpropdef} redefines type {mprop.full_name}", 4)
+		end
 		set_doc(mpropdef, modelbuilder)
 
 		var atfixed = get_single_annotation("fixed", modelbuilder)
@@ -1135,13 +1597,13 @@ redef class ATypePropdef
 	redef fun build_signature(modelbuilder)
 	do
 		var mpropdef = self.mpropdef
-		if mpropdef == null then return # Error thus skiped
+		if mpropdef == null then return # Error thus skipped
 		var mclassdef = mpropdef.mclassdef
 		var mmodule = mclassdef.mmodule
 		var mtype: nullable MType = null
 
 		var ntype = self.n_type
-		mtype = modelbuilder.resolve_mtype(mmodule, mclassdef, ntype)
+		mtype = modelbuilder.resolve_mtype_unchecked(mmodule, mclassdef, ntype, true)
 		if mtype == null then return
 
 		mpropdef.bound = mtype
@@ -1151,10 +1613,10 @@ redef class ATypePropdef
 	redef fun check_signature(modelbuilder)
 	do
 		var mpropdef = self.mpropdef
-		if mpropdef == null then return # Error thus skiped
+		if mpropdef == null then return # Error thus skipped
 
-		var bound = self.mpropdef.bound
-		if bound == null then return # Error thus skiped
+		var bound = mpropdef.bound
+		if bound == null then return # Error thus skipped
 
 		modelbuilder.check_visibility(n_type, bound, mpropdef)
 
@@ -1162,29 +1624,18 @@ redef class ATypePropdef
 		var mmodule = mclassdef.mmodule
 		var anchor = mclassdef.bound_mtype
 
-		# Check circularity
-		if bound isa MVirtualType then
-			# Slow case: progress on each resolution until: (i) we loop, or (ii) we found a non formal type
-			var seen = [self.mpropdef.mproperty.mvirtualtype]
-			loop
-				if seen.has(bound) then
-					seen.add(bound)
-					modelbuilder.error(self, "Error: circularity of virtual type definition: {seen.join(" -> ")}")
-					return
-				end
-				seen.add(bound)
-				var next = bound.lookup_bound(mmodule, anchor)
-				if not next isa MVirtualType then break
-				bound = next
-			end
+		var ntype = self.n_type
+		if modelbuilder.resolve_mtype(mmodule, mclassdef, ntype) == null then
+			mpropdef.bound = null
+			return
 		end
 
 		# Check redefinitions
-		bound = mpropdef.bound.as(not null)
 		for p in mpropdef.mproperty.lookup_super_definitions(mmodule, anchor) do
-			var supbound = p.bound.as(not null)
+			var supbound = p.bound
+			if supbound == null then break # broken super bound, skip error
 			if p.is_fixed then
-				modelbuilder.error(self, "Redef Error: Virtual type {mpropdef.mproperty} is fixed in super-class {p.mclassdef.mclass}")
+				modelbuilder.error(self, "Redef Error: virtual type `{mpropdef.mproperty}` is fixed in super-class `{p.mclassdef.mclass}`.")
 				break
 			end
 			if p.mclassdef.mclass == mclassdef.mclass then
@@ -1192,8 +1643,8 @@ redef class ATypePropdef
 				modelbuilder.warning(n_type, "refine-type", "Redef Error: a virtual type cannot be refined.")
 				break
 			end
-			if not bound.is_subtype(mmodule, anchor, supbound) then
-				modelbuilder.error(n_type, "Redef Error: Wrong bound type. Found {bound}, expected a subtype of {supbound}, as in {p}.")
+			if not modelbuilder.check_subtype(n_type, mmodule, anchor, bound, supbound) then
+				modelbuilder.error(n_type, "Redef Error: expected `{supbound}` bound type; got `{bound}`.")
 				break
 			end
 		end