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

diff --git a/src/model/model.nit b/src/model/model.nit
index 635d34a..d4d2c1c 100644
--- a/src/model/model.nit
+++ b/src/model/model.nit
@@ -14,24 +14,21 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
-# Object model of the Nit language
+# Classes, types and properties
 #
-# This module define the entities of the Nit meta-model like modules,
-# classes, types and properties
+# All three concepts are defined in this same module because these are strongly connected:
+# * types are based on classes
+# * classes contains properties
+# * some properties are types (virtual types)
 #
-# It also provide an API to build and query models.
-#
-# All model classes starts with the M letter (MModule, MClass, etc.)
-#
-# TODO: better doc
-#
-# TODO: liearization, closures, extern stuff
+# TODO: liearization, extern stuff
 # FIXME: better handling of the types
 module model
 
-import poset
-import location
-import model_base
+import mmodule
+import mdoc
+import ordered_tree
+private import more_collections
 
 redef class Model
 	# All known classes
@@ -69,7 +66,7 @@ redef class Model
 	# Collections of classes grouped by their short name
 	private var mclasses_by_name: MultiHashMap[String, MClass] = new MultiHashMap[String, MClass]
 
-	# Return all class named `name'.
+	# Return all class named `name`.
 	#
 	# If such a class does not exist, null is returned
 	# (instead of an empty array)
@@ -87,7 +84,7 @@ redef class Model
 	# Collections of properties grouped by their short name
 	private var mproperties_by_name: MultiHashMap[String, MProperty] = new MultiHashMap[String, MProperty]
 
-	# Return all properties named `name'.
+	# Return all properties named `name`.
 	#
 	# If such a property does not exist, null is returned
 	# (instead of an empty array)
@@ -104,6 +101,35 @@ redef class Model
 
 	# The only null type
 	var null_type: MNullType = new MNullType(self)
+
+	# Build an ordered tree with from `concerns`
+	fun concerns_tree(mconcerns: Collection[MConcern]): ConcernsTree do
+		var seen = new HashSet[MConcern]
+		var res = new ConcernsTree
+
+		var todo = new Array[MConcern]
+		todo.add_all mconcerns
+
+		while not todo.is_empty do
+			var c = todo.pop
+			if seen.has(c) then continue
+			var pc = c.parent_concern
+			if pc == null then
+				res.add(null, c)
+			else
+				res.add(pc, c)
+				todo.add(pc)
+			end
+			seen.add(c)
+		end
+
+		return res
+	end
+end
+
+# An OrderedTree that can be easily refined for display purposes
+class ConcernsTree
+	super OrderedTree[MConcern]
 end
 
 redef class MModule
@@ -114,7 +140,7 @@ redef class MModule
 	# (introduction and refinement)
 	var mclassdefs: Array[MClassDef] = new Array[MClassDef]
 
-	# Does the current module has a given class `mclass'?
+	# Does the current module has a given class `mclass`?
 	# Return true if the mmodule introduces, refines or imports a class.
 	# Visibility is not considered.
 	fun has_mclass(mclass: MClass): Bool
@@ -139,6 +165,7 @@ redef class MModule
 		for m in self.in_importation.greaters do
 			for cd in m.mclassdefs do
 				var c = cd.mclass
+				res.add_node(c)
 				for s in cd.supertypes do
 					res.add_edge(c, s.mclass)
 				end
@@ -148,9 +175,34 @@ redef class MModule
 		return res
 	end
 
+	# Sort a given array of classes using the linerarization order of the module
+	# The most general is first, the most specific is last
+	fun linearize_mclasses(mclasses: Array[MClass])
+	do
+		self.flatten_mclass_hierarchy.sort(mclasses)
+	end
+
+	# Sort a given array of class definitions using the linerarization order of the module
+	# the refinement link is stronger than the specialisation link
+	# The most general is first, the most specific is last
+	fun linearize_mclassdefs(mclassdefs: Array[MClassDef])
+	do
+		var sorter = new MClassDefSorter(self)
+		sorter.sort(mclassdefs)
+	end
+
+	# Sort a given array of property definitions using the linerarization order of the module
+	# the refinement link is stronger than the specialisation link
+	# The most general is first, the most specific is last
+	fun linearize_mpropdefs(mpropdefs: Array[MPropDef])
+	do
+		var sorter = new MPropDefSorter(self)
+		sorter.sort(mpropdefs)
+	end
+
 	private var flatten_mclass_hierarchy_cache: nullable POSet[MClass] = null
 
-	# The primitive type Object, the root of the class hierarchy
+	# The primitive type `Object`, the root of the class hierarchy
 	fun object_type: MClassType
 	do
 		var res = self.object_type_cache
@@ -162,7 +214,7 @@ redef class MModule
 
 	private var object_type_cache: nullable MClassType
 
-	# The primitive type Bool
+	# The primitive type `Bool`
 	fun bool_type: MClassType
 	do
 		var res = self.bool_type_cache
@@ -174,7 +226,7 @@ redef class MModule
 
 	private var bool_type_cache: nullable MClassType
 
-	# The primitive type Sys, the main type of the program, if any
+	# The primitive type `Sys`, the main type of the program, if any
 	fun sys_type: nullable MClassType
 	do
 		var clas = self.model.get_mclasses_by_name("Sys")
@@ -182,7 +234,14 @@ redef class MModule
 		return get_primitive_class("Sys").mclass_type
 	end
 
-	# Force to get the primitive class named `name' or abort
+	fun finalizable_type: nullable MClassType
+	do
+		var clas = self.model.get_mclasses_by_name("Finalizable")
+		if clas == null then return null
+		return get_primitive_class("Finalizable").mclass_type
+	end
+
+	# Force to get the primitive class named `name` or abort
 	fun get_primitive_class(name: String): MClass
 	do
 		var cla = self.model.get_mclasses_by_name(name)
@@ -195,41 +254,89 @@ redef class MModule
 			print("Fatal Error: no primitive class {name}")
 			exit(1)
 		end
-		assert cla.length == 1 else print cla.join(", ")
+		if cla.length != 1 then
+			var msg = "Fatal Error: more than one primitive class {name}:"
+			for c in cla do msg += " {c.full_name}"
+			print msg
+			exit(1)
+		end
 		return cla.first
 	end
 
-	# Try to get the primitive method named `name' on the type `recv'
-	fun try_get_primitive_method(name: String, recv: MType): nullable MMethod
+	# Try to get the primitive method named `name` on the type `recv`
+	fun try_get_primitive_method(name: String, recv: MClass): nullable MMethod
 	do
 		var props = self.model.get_mproperties_by_name(name)
 		if props == null then return null
 		var res: nullable MMethod = null
 		for mprop in props do
 			assert mprop isa MMethod
-			if not recv.has_mproperty(self, mprop) then continue
-			if res == null then
-				res = mprop
-			else
-				print("Fatal Error: ambigous property name '{name}'; conflict between {mprop.full_name} and {res.full_name}")
-				abort
+			var intro = mprop.intro_mclassdef
+			for mclassdef in recv.mclassdefs do
+				if not self.in_importation.greaters.has(mclassdef.mmodule) then continue
+				if not mclassdef.in_hierarchy.greaters.has(intro) then continue
+				if res == null then
+					res = mprop
+				else if res != mprop then
+					print("Fatal Error: ambigous property name '{name}'; conflict between {mprop.full_name} and {res.full_name}")
+					abort
+				end
 			end
 		end
 		return res
 	end
 end
 
+private class MClassDefSorter
+	super AbstractSorter[MClassDef]
+	var mmodule: MModule
+	redef fun compare(a, b)
+	do
+		var ca = a.mclass
+		var cb = b.mclass
+		if ca != cb then return mmodule.flatten_mclass_hierarchy.compare(ca, cb)
+		return mmodule.model.mclassdef_hierarchy.compare(a, b)
+	end
+end
+
+private class MPropDefSorter
+	super AbstractSorter[MPropDef]
+	var mmodule: MModule
+	redef fun compare(pa, pb)
+	do
+		var a = pa.mclassdef
+		var b = pb.mclassdef
+		var ca = a.mclass
+		var cb = b.mclass
+		if ca != cb then return mmodule.flatten_mclass_hierarchy.compare(ca, cb)
+		return mmodule.model.mclassdef_hierarchy.compare(a, b)
+	end
+end
+
 # A named class
 #
-# MClass are global to the model; it means that a MClass is not bound to a
+# `MClass` are global to the model; it means that a `MClass` is not bound to a
 # specific `MModule`.
 #
 # This characteristic helps the reasoning about classes in a program since a
-# single MClass object always denote the same class.
-# However, because a MClass is global, it does not really have properties nor
-# belong to a hierarchy since the property and the
-# hierarchy of a class depends of a module.
+# single `MClass` object always denote the same class.
+#
+# The drawback is that classes (`MClass`) contain almost nothing by themselves.
+# These do not really have properties nor belong to a hierarchy since the property and the
+# hierarchy of a class depends of the refinement in the modules.
+#
+# Most services on classes require the precision of a module, and no one can asks what are
+# the super-classes of a class nor what are properties of a class without precising what is
+# the module considered.
+#
+# For instance, during the typing of a source-file, the module considered is the module of the file.
+# eg. the question *is the method `foo` exists in the class `Bar`?* must be reformulated into
+# *is the method `foo` exists in the class `Bar` in the current module?*
+#
+# During some global analysis, the module considered may be the main module of the program.
 class MClass
+	super MEntity
+
 	# The module that introduce the class
 	# While classes are not bound to a specific module,
 	# the introducing module is used for naming an visibility
@@ -237,10 +344,10 @@ class MClass
 
 	# The short name of the class
 	# In Nit, the name of a class cannot evolve in refinements
-	var name: String
+	redef var name: String
 
 	# The canonical name of the class
-	# Example: "owner::module::MyClass"
+	# Example: `"owner::module::MyClass"`
 	fun full_name: String
 	do
 		return "{self.intro_mmodule.full_name}::{name}"
@@ -285,14 +392,16 @@ class MClass
 		end
 	end
 
+	redef fun model do return intro_mmodule.model
+
 	# All class definitions (introduction and refinements)
 	var mclassdefs: Array[MClassDef] = new Array[MClassDef]
 
-	# Alias for `name'
+	# Alias for `name`
 	redef fun to_s do return self.name
 
 	# The definition that introduced the class
-	# Warning: the introduction is the first `MClassDef' object associated
+	# Warning: the introduction is the first `MClassDef` object associated
 	# to self.  If self is just created without having any associated
 	# definition, this method will abort
 	fun intro: MClassDef
@@ -301,10 +410,10 @@ class MClass
 		return mclassdefs.first
 	end
 
-	# Return the class `self' in the class hierarchy of the module `mmodule'.
+	# Return the class `self` in the class hierarchy of the module `mmodule`.
 	#
-	# SEE: MModule::flatten_mclass_hierarchy
-	# REQUIRE: mmodule.has_mclass(self)
+	# SEE: `MModule::flatten_mclass_hierarchy`
+	# REQUIRE: `mmodule.has_mclass(self)`
 	fun in_hierarchy(mmodule: MModule): POSetElement[MClass]
 	do
 		return mmodule.flatten_mclass_hierarchy[self]
@@ -312,25 +421,25 @@ class MClass
 
 	# The principal static type of the class.
 	#
-	# For non-generic class, mclass_type is the only MClassType based
+	# For non-generic class, mclass_type is the only `MClassType` based
 	# on self.
 	#
 	# For a generic class, the arguments are the formal parameters.
-	# i.e.: for the class `Array[E:Object]', the mtype is Array[E].
-	# If you want `Array[Object]' the see `MClassDef::bound_mtype'
+	# i.e.: for the class Array[E:Object], the `mclass_type` is Array[E].
+	# If you want Array[Object] the see `MClassDef::bound_mtype`
 	#
 	# For generic classes, the mclass_type is also the way to get a formal
 	# generic parameter type.
 	#
-	# To get other types based on a generic class, see `get_mtype'.
+	# To get other types based on a generic class, see `get_mtype`.
 	#
-	# ENSURE: mclass_type.mclass == self
+	# ENSURE: `mclass_type.mclass == self`
 	var mclass_type: MClassType
 
 	# Return a generic type based on the class
-	# Is the class is not generic, then the result is `mclass_type'
+	# Is the class is not generic, then the result is `mclass_type`
 	#
-	# REQUIRE: type_arguments.length == self.arity
+	# REQUIRE: `mtype_arguments.length == self.arity`
 	fun get_mtype(mtype_arguments: Array[MType]): MClassType
 	do
 		assert mtype_arguments.length == self.arity
@@ -351,26 +460,35 @@ end
 
 # A definition (an introduction or a refinement) of a class in a module
 #
-# A MClassDef is associated with an explicit (or almost) definition of a
-# class. Unlike MClass, a MClassDef is a local definition that belong to
-# a specific module
+# A `MClassDef` is associated with an explicit (or almost) definition of a
+# class. Unlike `MClass`, a `MClassDef` is a local definition that belong to
+# a specific class and a specific module, and contains declarations like super-classes
+# or properties.
+#
+# It is the class definitions that are the backbone of most things in the model:
+# ClassDefs are defined with regard with other classdefs.
+# Refinement and specialization are combined to produce a big poset called the `Model::mclassdef_hierarchy`.
+#
+# Moreover, the extension and the intention of types is defined by looking at the MClassDefs.
 class MClassDef
+	super MEntity
+
 	# The module where the definition is
 	var mmodule: MModule
 
-	# The associated MClass
+	# The associated `MClass`
 	var mclass: MClass
 
 	# The bounded type associated to the mclassdef
 	#
-	# For a non-generic class, `bound_mtype' and `mclass.mclass_type'
+	# For a non-generic class, `bound_mtype` and `mclass.mclass_type`
 	# are the same type.
 	#
 	# Example:
 	# For the classdef Array[E: Object], the bound_mtype is Array[Object].
-	# If you want Array[E], then see `mclass.mclass_type'
+	# If you want Array[E], then see `mclass.mclass_type`
 	#
-	# ENSURE: bound_mtype.mclass = self.mclass
+	# ENSURE: `bound_mtype.mclass == self.mclass`
 	var bound_mtype: MClassType
 
 	# Name of each formal generic parameter (in order of declaration)
@@ -381,7 +499,7 @@ class MClassDef
 
 	# Internal name combining the module and the class
 	# Example: "mymodule#MyClass"
-	redef fun to_s do return "{mmodule}#{mclass}"
+	redef var to_s: String
 
 	init(mmodule: MModule, bound_mtype: MClassType, location: Location, parameter_names: Array[String])
 	do
@@ -393,8 +511,14 @@ class MClassDef
 		mmodule.mclassdefs.add(self)
 		mclass.mclassdefs.add(self)
 		self.parameter_names = parameter_names
+		self.to_s = "{mmodule}#{mclass}"
 	end
 
+	# Actually the name of the `mclass`
+	redef fun name do return mclass.name
+
+	redef fun model do return mmodule.model
+
 	# All declared super-types
 	# FIXME: quite ugly but not better idea yet
 	var supertypes: Array[MClassType] = new Array[MClassType]
@@ -402,7 +526,7 @@ class MClassDef
 	# Register some super-types for the class (ie "super SomeType")
 	#
 	# The hierarchy must not already be set
-	# REQUIRE: self.in_hierarchy == null
+	# REQUIRE: `self.in_hierarchy == null`
 	fun set_supertypes(supertypes: Array[MClassType])
 	do
 		assert unique_invocation: self.in_hierarchy == null
@@ -426,8 +550,8 @@ class MClassDef
 	# Collect the super-types (set by set_supertypes) to build the hierarchy
 	#
 	# This function can only invoked once by class
-	# REQUIRE: self.in_hierarchy == null
-	# ENSURE: self.in_hierarchy != null
+	# REQUIRE: `self.in_hierarchy == null`
+	# ENSURE: `self.in_hierarchy != null`
 	fun add_in_hierarchy
 	do
 		assert unique_invocation: self.in_hierarchy == null
@@ -443,7 +567,7 @@ class MClassDef
 		end
 	end
 
-	# The view of the class definition in `mclassdef_hierarchy'
+	# The view of the class definition in `mclassdef_hierarchy`
 	var in_hierarchy: nullable POSetElement[MClassDef] = null
 
 	# Is the definition the one that introduced `mclass`?
@@ -458,12 +582,12 @@ end
 
 # A global static type
 #
-# MType are global to the model; it means that a MType is not bound to a
+# MType are global to the model; it means that a `MType` is not bound to a
 # specific `MModule`.
 # This characteristic helps the reasoning about static types in a program
-# since a single MType object always denote the same type.
+# since a single `MType` object always denote the same type.
 #
-# However, because a MType is global, it does not really have properties
+# However, because a `MType` is global, it does not really have properties
 # nor have subtypes to a hierarchy since the property and the class hierarchy
 # depends of a module.
 # Moreover, virtual types an formal generic parameter types also depends on
@@ -475,29 +599,24 @@ end
 # The anchor is used to know what is the bound of the virtual types and formal
 # generic parameter types.
 #
-# MType are not directly usable to get properties. See the `anchor_to' method
-# and the `MClassType' class.
+# MType are not directly usable to get properties. See the `anchor_to` method
+# and the `MClassType` class.
 #
 # FIXME: the order of the parameters is not the best. We mus pick on from:
 #  * foo(mmodule, anchor, othertype)
 #  * foo(othertype, anchor, mmodule)
 #  * foo(anchor, mmodule, othertype)
 #  * foo(othertype, mmodule, anchor)
-#
-# FIXME: Add a 'is_valid_anchor' to improve imputability.
-# Currently, anchors are used "as it" without check thus if the caller gives a
-# bad anchor, then the method will likely crash (abort) in a bad case
-#
-# FIXME: maybe allways add an anchor with a nullable type (as in is_subtype)
 abstract class MType
+	super MEntity
 
-	# The model of the type
-	fun model: Model is abstract
+	redef fun name do return to_s
 
-	# Return true if `self' is an subtype of `sup'.
+	# Return true if `self` is an subtype of `sup`.
 	# The typing is done using the standard typing policy of Nit.
 	#
-	# REQUIRE: anchor == null implies not self.need_anchor and not sup.need_anchor
+	# REQUIRE: `anchor == null implies not self.need_anchor and not sup.need_anchor`
+	# REQUIRE: `anchor != null implies self.can_resolve_for(anchor, null, mmodule) and sup.can_resolve_for(anchor, null, mmodule)`
 	fun is_subtype(mmodule: MModule, anchor: nullable MClassType, sup: MType): Bool
 	do
 		var sub = self
@@ -505,44 +624,76 @@ abstract class MType
 		if anchor == null then
 			assert not sub.need_anchor
 			assert not sup.need_anchor
+		else
+			assert sub.can_resolve_for(anchor, null, mmodule)
+			assert sup.can_resolve_for(anchor, null, mmodule)
 		end
-		# First, resolve the types
+
+		# First, resolve the formal types to a common version in the receiver
+		# The trick here is that fixed formal type will be associed to the bound
+		# And unfixed formal types will be associed to a canonical formal type.
 		if sub isa MParameterType or sub isa MVirtualType then
 			assert anchor != null
-			sub = sub.resolve_for(anchor, anchor, mmodule, false)
+			sub = sub.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, false)
 		end
 		if sup isa MParameterType or sup isa MVirtualType then
 			assert anchor != null
-			sup = sup.resolve_for(anchor, anchor, mmodule, false)
+			sup = sup.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, false)
+		end
+
+		# Does `sup` accept null or not?
+		# Discard the nullable marker if it exists
+		var sup_accept_null = false
+		if sup isa MNullableType then
+			sup_accept_null = true
+			sup = sup.mtype
+		else if sup isa MNullType then
+			sup_accept_null = true
+		end
+
+		# Can `sub` provide null or not?
+		# Thus we can match with `sup_accept_null`
+		# Also discard the nullable marker if it exists
+		if sub isa MNullableType then
+			if not sup_accept_null then return false
+			sub = sub.mtype
+		else if sub isa MNullType then
+			return sup_accept_null
 		end
+		# Now the case of direct null and nullable is over.
 
-		if sup isa MParameterType or sup isa MVirtualType or sup isa MNullType then
+		# A unfixed formal type can only accept itself
+		if sup isa MParameterType or sup isa MVirtualType then
 			return sub == sup
 		end
+
+		# If `sub` is a formal type, then it is accepted if its bound is accepted
 		if sub isa MParameterType or sub isa MVirtualType then
 			assert anchor != null
 			sub = sub.anchor_to(mmodule, anchor)
-		end
-		if sup isa MNullableType then
-			if sub isa MNullType then
-				return true
-			else if sub isa MNullableType then
-				return sub.mtype.is_subtype(mmodule, anchor, sup.mtype)
-			else if sub isa MClassType then
-				return sub.is_subtype(mmodule, anchor, sup.mtype)
-			else
-				abort
+
+			# Manage the second layer of null/nullable
+			if sub isa MNullableType then
+				if not sup_accept_null then return false
+				sub = sub.mtype
+			else if sub isa MNullType then
+				return sup_accept_null
 			end
 		end
 
-		assert sup isa MClassType # It is the only remaining type
-		if sub isa MNullableType or sub isa MNullType then
+		assert sub isa MClassType # It is the only remaining type
+
+		if sup isa MNullType then
+			# `sup` accepts only null
 			return false
 		end
 
+		assert sup isa MClassType # It is the only remaining type
+
+		# Now both are MClassType, we need to dig
+
 		if sub == sup then return true
 
-		assert sub isa MClassType # It is the only remaining type
 		if anchor == null then anchor = sub # UGLY: any anchor will work
 		var resolved_sub = sub.anchor_to(mmodule, anchor)
 		var res = resolved_sub.collect_mclasses(mmodule).has(sup.mclass)
@@ -571,34 +722,38 @@ abstract class MType
 	# types to their bounds.
 	#
 	# Example
+	#     class A end
+	#     class B super A end
+	#     class X end
+	#     class Y super X end
 	#     class G[T: A]
 	#       type U: X
 	#     end
 	#     class H
-	#       super G[C]
+	#       super G[B]
 	#       redef type U: Y
 	#     end
-	# Map[T,U]  anchor_to  H  #->  Map[C,Y]
+	# Map[T,U]  anchor_to  H  #->  Map[B,Y]
 	#
 	# Explanation of the example:
-	# In H, T is set to C, because "H super G[C]", and U is bound to Y,
+	# In H, T is set to B, because "H super G[B]", and U is bound to Y,
         # because "redef type U: Y". Therefore, Map[T, U] is bound to
-	# Map[C, Y]
+	# Map[B, Y]
 	#
-	# ENSURE: not self.need_anchor implies return == self
-	# ENSURE: not return.need_anchor
+	# ENSURE: `not self.need_anchor implies result == self`
+	# ENSURE: `not result.need_anchor`
 	fun anchor_to(mmodule: MModule, anchor: MClassType): MType
 	do
 		if not need_anchor then return self
 		assert not anchor.need_anchor
 		# Just resolve to the anchor and clear all the virtual types
-		var res = self.resolve_for(anchor, anchor, mmodule, true)
+		var res = self.resolve_for(anchor, null, mmodule, true)
 		assert not res.need_anchor
 		return res
 	end
 
-	# Does `self' contain a virtual type or a formal generic parameter type?
-	# In order to remove those types, you usually want to use `anchor_to'.
+	# Does `self` contain a virtual type or a formal generic parameter type?
+	# In order to remove those types, you usually want to use `anchor_to`.
 	fun need_anchor: Bool do return true
 
 	# Return the supertype when adapted to a class.
@@ -606,17 +761,24 @@ abstract class MType
 	# In Nit, for each super-class of a type, there is a equivalent super-type.
 	#
 	# Example:
-	#     class G[T, U]
-	#     class H[V] super G[V, Bool]
+	#     class G[T, U] end
+	#     class H[V] super G[V, Bool] end
 	# H[Int]  supertype_to  G  #->  G[Int, Bool]
 	#
-	# REQUIRE: `super_mclass' is a super-class of `self'
-	# ENSURE: return.mclass = mclass
-	fun supertype_to(mmodule: MModule, anchor: MClassType, super_mclass: MClass): MClassType
+	# REQUIRE: `super_mclass` is a super-class of `self`
+	# REQUIRE: `self.need_anchor implies anchor != null and self.can_resolve_for(anchor, null, mmodule)`
+	# ENSURE: `result.mclass = super_mclass`
+	fun supertype_to(mmodule: MModule, anchor: nullable MClassType, super_mclass: MClass): MClassType
 	do
 		if super_mclass.arity == 0 then return super_mclass.mclass_type
 		if self isa MClassType and self.mclass == super_mclass then return self
-		var resolved_self = self.anchor_to(mmodule, anchor)
+		var resolved_self
+		if self.need_anchor then
+			assert anchor != null
+			resolved_self = self.anchor_to(mmodule, anchor)
+		else
+			resolved_self = self
+		end
 		var supertypes = resolved_self.collect_mtypes(mmodule)
 		for supertype in supertypes do
 			if supertype.mclass == super_mclass then
@@ -627,51 +789,100 @@ abstract class MType
 		abort
 	end
 
-	# Replace formals generic types in self with resolved values in `mtype'
-	# If `cleanup_virtual' is true, then virtual types are also replaced
-	# with their bounds
+	# Replace formals generic types in self with resolved values in `mtype`
+	# If `cleanup_virtual` is true, then virtual types are also replaced
+	# with their bounds.
 	#
-	# This function returns self if `need_anchor' is false.
+	# This function returns self if `need_anchor` is false.
 	#
-	# Example:
-	#     class G[E]
-	#     class H[F] super G[F]
-	# Array[E]  resolve_for  H[Int]  #->  Array[Int]
+	# ## Example 1
+	#
+	#     class G[E] end
+	#     class H[F] super G[F] end
+	#     class X[Z] end
+	#
+	#  * Array[E].resolve_for(H[Int])  #->  Array[Int]
+	#  * Array[E].resolve_for(G[Z], X[Int]) #->  Array[Z]
 	#
 	# Explanation of the example:
-	#  * Array[E].need_anchor is true because there is a formal generic
-	#    parameter type E
-	#  * E makes sense for H[Int] because E is a formal parameter of G
-	#    and H specialize G
+	#  * Array[E].need_anchor is true because there is a formal generic parameter type E
+	#  * E makes sense for H[Int] because E is a formal parameter of G and H specialize G
 	#  * Since "H[F] super G[F]", E is in fact F for H
 	#  * More specifically, in H[Int], E is Int
 	#  * So, in H[Int], Array[E] is Array[Int]
 	#
 	# This function is mainly used to inherit a signature.
-	# Because, unlike `anchor_type', we do not want a full resolution of
+	# Because, unlike `anchor_to`, we do not want a full resolution of
 	# a type but only an adapted version of it.
 	#
-	# Example:
-        #     class A[E]
-	#         foo(e:E):E
+	# ## Example 2
+	#
+	#     class A[E]
+	#         fun foo(e:E):E is abstract
 	#     end
 	#     class B super A[Int] end
 	#
 	# The signature on foo is (e: E): E
 	# If we resolve the signature for B, we get (e:Int):Int
 	#
-	# TODO: Explain the cleanup_virtual
+	# ## Example 3
+	#
+	#     class A[E]
+	#         fun foo(e:E) is abstract
+	#     end
+	#     class B[F]
+	#         var a: A[Array[F]]
+	#         fun bar do a.foo(x) # <- x is here
+	#     end
+	#
+	# The first question is: is foo available on `a`?
+	#
+	# The static type of a is `A[Array[F]]`, that is an open type.
+	# in order to find a method `foo`, whe must look at a resolved type.
+	#
+	#   A[Array[F]].anchor_to(B[nullable Object])  #->  A[Array[nullable Object]]
 	#
-	# FIXME: the parameter `cleanup_virtual' is just a bad idea, but having
+	# the method `foo` exists in `A[Array[nullable Object]]`, therefore `foo` exists for `a`.
+	#
+	# The next question is: what is the accepted types for `x`?
+	#
+	# the signature of `foo` is `foo(e:E)`, thus we must resolve the type E
+	#
+	#   E.resolve_for(A[Array[F]],B[nullable Object])  #->  Array[F]
+	#
+	# The resolution can be done because `E` make sense for the class A (see `can_resolve_for`)
+	#
+	# FIXME: the parameter `cleanup_virtual` is just a bad idea, but having
 	# two function instead of one seems also to be a bad idea.
 	#
-	# ENSURE: not self.need_anchor implies return == self
-	fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract
+	# REQUIRE: `can_resolve_for(mtype, anchor, mmodule)`
+	# ENSURE: `not self.need_anchor implies result == self`
+	fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract
+
+	# Can the type be resolved?
+	#
+	# In order to resolve open types, the formal types must make sence.
+	#
+	# ## Example
+	#
+	#     class A[E]
+	#     end
+	#     class B[F]
+	#     end
+	#
+	#  * E.can_resolve_for(A[Int])  #->  true, E make sense in A
+	#  * E.can_resolve_for(B[Int])  #->  false, E does not make sense in B
+	#  * B[E].can_resolve_for(A[F], B[Object])  #->  true,
+	#    B[E] is a red hearing only the E is important,
+	#    E make sense in A
+	#
+	# REQUIRE: `anchor != null implies not anchor.need_anchor`
+	# REQUIRE: `mtype.need_anchor implies anchor != null and mtype.can_resolve_for(anchor, null, mmodule)`
+	# ENSURE: `not self.need_anchor implies result == true`
+	fun can_resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule): Bool is abstract
 
 	# Return the nullable version of the type
 	# If the type is already nullable then self is returned
-	#
-	# FIXME: DO NOT WORK YET
 	fun as_nullable: MType
 	do
 		var res = self.as_nullable_cache
@@ -681,8 +892,45 @@ abstract class MType
 		return res
 	end
 
+	# Return the not nullable version of the type
+	# Is the type is already not nullable, then self is returned.
+	#
+	# Note: this just remove the `nullable` notation, but the result can still contains null.
+	# For instance if `self isa MNullType` or self is a a formal type bounded by a nullable type.
+	fun as_notnullable: MType
+	do
+		return self
+	end
+
 	private var as_nullable_cache: nullable MType = null
 
+
+	# The deph of the type seen as a tree.
+	#
+	# * A -> 1
+	# * G[A] -> 2
+	# * H[A, B] -> 2
+	# * H[G[A], B] -> 3
+	#
+	# Formal types have a depth of 1.
+	fun depth: Int
+	do
+		return 1
+	end
+
+	# The length of the type seen as a tree.
+	#
+	# * A -> 1
+	# * G[A] -> 2
+	# * H[A, B] -> 3
+	# * H[G[A], B] -> 4
+	#
+	# Formal types have a length of 1.
+	fun length: Int
+	do
+		return 1
+	end
+
 	# Compute all the classdefs inherited/imported.
 	# The returned set contains:
 	#  * the class definitions from `mmodule` and its imported modules
@@ -690,26 +938,26 @@ abstract class MType
 	#
 	# This function is used mainly internally.
 	#
-	# REQUIRE: not self.need_anchor
+	# REQUIRE: `not self.need_anchor`
 	fun collect_mclassdefs(mmodule: MModule): Set[MClassDef] is abstract
 
 	# Compute all the super-classes.
 	# This function is used mainly internally.
 	#
-	# REQUIRE: not self.need_anchor
+	# REQUIRE: `not self.need_anchor`
 	fun collect_mclasses(mmodule: MModule): Set[MClass] is abstract
 
 	# Compute all the declared super-types.
 	# Super-types are returned as declared in the classdefs (verbatim).
 	# This function is used mainly internally.
 	#
-	# REQUIRE: not self.need_anchor
+	# REQUIRE: `not self.need_anchor`
 	fun collect_mtypes(mmodule: MModule): Set[MClassType] is abstract
 
 	# Is the property in self for a given module
 	# This method does not filter visibility or whatever
 	#
-	# REQUIRE: not self.need_anchor
+	# REQUIRE: `not self.need_anchor`
 	fun has_mproperty(mmodule: MModule, mproperty: MProperty): Bool
 	do
 		assert not self.need_anchor
@@ -719,7 +967,7 @@ end
 
 # A type based on a class.
 #
-# MClassType have properties (see `has_property').
+# `MClassType` have properties (see `has_mproperty`).
 class MClassType
 	super MType
 
@@ -734,7 +982,7 @@ class MClassType
 	end
 
 	# The formal arguments of the type
-	# ENSURE: return.length == self.mclass.arity
+	# ENSURE: `result.length == self.mclass.arity`
 	var arguments: Array[MType] = new Array[MType]
 
 	redef fun to_s do return mclass.to_s
@@ -746,7 +994,9 @@ class MClassType
 		return super.as(MClassType)
 	end
 
-	redef fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MClassType do return self
+	redef fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MClassType do return self
+
+	redef fun can_resolve_for(mtype, anchor, mmodule) do return true
 
 	redef fun collect_mclassdefs(mmodule)
 	do
@@ -778,7 +1028,7 @@ class MClassType
 		return cache[mmodule]
 	end
 
-	# common implementation for `collect_mclassdefs', `collect_mclasses', and `collect_mtypes'.
+	# common implementation for `collect_mclassdefs`, `collect_mclasses`, and `collect_mtypes`.
 	private fun collect_things(mmodule: MModule)
 	do
 		var res = new HashSet[MClassDef]
@@ -832,26 +1082,55 @@ class MGenericType
 				break
 			end
 		end
+
+		self.to_s = "{mclass}[{arguments.join(", ")}]"
 	end
 
 	# Recursively print the type of the arguments within brackets.
-	# Example: "Map[String,List[Int]]"
-	redef fun to_s
-	do
-		return "{mclass}[{arguments.join(",")}]"
-	end
+	# Example: `"Map[String, List[Int]]"`
+	redef var to_s: String
 
 	redef var need_anchor: Bool
 
 	redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 	do
 		if not need_anchor then return self
+		assert can_resolve_for(mtype, anchor, mmodule)
 		var types = new Array[MType]
 		for t in arguments do
 			types.add(t.resolve_for(mtype, anchor, mmodule, cleanup_virtual))
 		end
 		return mclass.get_mtype(types)
 	end
+
+	redef fun can_resolve_for(mtype, anchor, mmodule)
+	do
+		if not need_anchor then return true
+		for t in arguments do
+			if not t.can_resolve_for(mtype, anchor, mmodule) then return false
+		end
+		return true
+	end
+
+
+	redef fun depth
+	do
+		var dmax = 0
+		for a in self.arguments do
+			var d = a.depth
+			if d > dmax then dmax = d
+		end
+		return dmax + 1
+	end
+
+	redef fun length
+	do
+		var res = 1
+		for a in self.arguments do
+			res += a.length
+		end
+		return res
+	end
 end
 
 # A virtual formal type.
@@ -889,20 +1168,67 @@ class MVirtualType
 		abort
 	end
 
+	# Is the virtual type fixed for a given resolved_receiver?
+	fun is_fixed(mmodule: MModule, resolved_receiver: MType): Bool
+	do
+		assert not resolved_receiver.need_anchor
+		var props = self.mproperty.lookup_definitions(mmodule, resolved_receiver)
+		if props.is_empty then
+			abort
+		end
+		for p in props do
+			if p.as(MVirtualTypeDef).is_fixed then return true
+		end
+		return false
+	end
+
 	redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 	do
-		if not cleanup_virtual then return self
+		assert can_resolve_for(mtype, anchor, mmodule)
 		# self is a virtual type declared (or inherited) in mtype
 		# The point of the function it to get the bound of the virtual type that make sense for mtype
 		# But because mtype is maybe a virtual/formal type, we need to get a real receiver first
 		#print "{class_name}: {self}/{mtype}/{anchor}?"
-		var resolved_reciever = mtype.resolve_for(anchor, anchor, mmodule, true)
+		var resolved_reciever
+		if mtype.need_anchor then
+			assert anchor != null
+			resolved_reciever = mtype.resolve_for(anchor, null, mmodule, true)
+		else
+			resolved_reciever = mtype
+		end
 		# Now, we can get the bound
 		var verbatim_bound = lookup_bound(mmodule, resolved_reciever)
 		# The bound is exactly as declared in the "type" property, so we must resolve it again
-		var res = verbatim_bound.resolve_for(mtype, anchor, mmodule, true)
+		var res = verbatim_bound.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 		#print "{class_name}: {self}/{mtype}/{anchor} -> {self}/{resolved_reciever}/{anchor} -> {verbatim_bound}/{mtype}/{anchor} -> {res}"
-		return res
+
+		# What to return here? There is a bunch a special cases:
+		# If 'cleanup_virtual' we must return the resolved type, since we cannot return self
+		if cleanup_virtual then return res
+		# If the reciever is a intern class, then the virtual type cannot be redefined since there is no possible subclass. self is just fixed. so simply return the resolution
+		if resolved_reciever isa MNullableType then resolved_reciever = resolved_reciever.mtype
+		if resolved_reciever.as(MClassType).mclass.kind == enum_kind then return res
+		# If the resolved type isa MVirtualType, it means that self was bound to it, and cannot be unbound. self is just fixed. so return the resolution.
+		if res isa MVirtualType then return res
+		# If we are final, just return the resolution
+		if is_fixed(mmodule, resolved_reciever) then return res
+		# It the resolved type isa intern class, then there is no possible valid redefinition is any potentiel subclass. self is just fixed. so simply return the resolution
+		if res isa MClassType and res.mclass.kind == enum_kind then return res
+		# TODO: Add 'fixed' virtual type in the specification.
+		# TODO: What if bound to a MParameterType?
+		# Note that Nullable types can always be redefined by the non nullable version, so there is no specific case on it.
+
+		# If anything apply, then `self' cannot be resolved, so return self
+		return self
+	end
+
+	redef fun can_resolve_for(mtype, anchor, mmodule)
+	do
+		if mtype.need_anchor then
+			assert anchor != null
+			mtype = mtype.anchor_to(mmodule, anchor)
+		end
+		return mtype.has_mproperty(mmodule, mproperty)
 	end
 
 	redef fun to_s do return self.mproperty.to_s
@@ -919,8 +1245,8 @@ end
 # It's mean that all refinements of a same class "share" the parameter type,
 # but that a generic subclass has its on parameter types.
 #
-# However, in the sense of the meta-model, the a parameter type of a class is
-# a valid types in a subclass. The "in the sense of the meta-model" is
+# However, in the sense of the meta-model, a parameter type of a class is
+# a valid type in a subclass. The "in the sense of the meta-model" is
 # important because, in the Nit language, the programmer cannot refers
 # directly to the parameter types of the super-classes.
 #
@@ -931,13 +1257,13 @@ end
 #     class B[F]
 #         super A[Array[F]]
 #     end
-# In the class definition B[F], `F' is a valid type but `E' is not.
-# However, `self.e' is a valid method call, and the signature of `e' is
-# declared `e: E'.
+# In the class definition B[F], `F` is a valid type but `E` is not.
+# However, `self.e` is a valid method call, and the signature of `e` is
+# declared `e: E`.
 #
 # Note that parameter types are shared among class refinements.
-# Therefore parameter only have an internal name (see `to_s' for details).
-# TODO: Add a 'name_for' to get better messages.
+# Therefore parameter only have an internal name (see `to_s` for details).
+# TODO: Add a `name_for` to get better messages.
 class MParameterType
 	super MType
 
@@ -947,7 +1273,7 @@ class MParameterType
 	redef fun model do return self.mclass.intro_mmodule.model
 
 	# The position of the parameter (0 for the first parameter)
-	# FIXME: is `position' a better name?
+	# FIXME: is `position` a better name?
 	var rank: Int
 
 	# Internal name of the parameter type
@@ -977,24 +1303,37 @@ class MParameterType
 
 	redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 	do
+		assert can_resolve_for(mtype, anchor, mmodule)
 		#print "{class_name}: {self}/{mtype}/{anchor}?"
 
 		if mtype isa MGenericType and mtype.mclass == self.mclass then
-			return mtype.arguments[self.rank]
+			var res = mtype.arguments[self.rank]
+			if anchor != null and res.need_anchor then
+				# Maybe the result can be resolved more if are bound to a final class
+				var r2 = res.anchor_to(mmodule, anchor)
+				if r2 isa MClassType and r2.mclass.kind == enum_kind then return r2
+			end
+			return res
 		end
 
 		# self is a parameter type of mtype (or of a super-class of mtype)
 		# The point of the function it to get the bound of the virtual type that make sense for mtype
 		# But because mtype is maybe a virtual/formal type, we need to get a real receiver first
 		# FIXME: What happend here is far from clear. Thus this part must be validated and clarified
-		var resolved_receiver = mtype.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, true)
+		var resolved_receiver
+		if mtype.need_anchor then
+			assert anchor != null
+			resolved_receiver = mtype.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, true)
+		else
+			resolved_receiver = mtype
+		end
 		if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
 		if resolved_receiver isa MParameterType then
 			assert resolved_receiver.mclass == anchor.mclass
 			resolved_receiver = anchor.arguments[resolved_receiver.rank]
 			if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
 		end
-		assert resolved_receiver isa MClassType else print "{class_name}: {self}/{mtype}/{anchor}? {resolved_receiver}"
+		assert resolved_receiver isa MClassType
 
 		# Eh! The parameter is in the current class.
 		# So we return the corresponding argument, no mater what!
@@ -1004,7 +1343,10 @@ class MParameterType
 			return res
 		end
 
-		resolved_receiver = resolved_receiver.resolve_for(anchor, anchor, mmodule, false)
+		if resolved_receiver.need_anchor then
+			assert anchor != null
+			resolved_receiver = resolved_receiver.resolve_for(anchor, null, mmodule, false)
+		end
 		# Now, we can get the bound
 		var verbatim_bound = lookup_bound(mmodule, resolved_receiver)
 		# The bound is exactly as declared in the "type" property, so we must resolve it again
@@ -1015,6 +1357,15 @@ class MParameterType
 		return res
 	end
 
+	redef fun can_resolve_for(mtype, anchor, mmodule)
+	do
+		if mtype.need_anchor then
+			assert anchor != null
+			mtype = mtype.anchor_to(mmodule, anchor)
+		end
+		return mtype.collect_mclassdefs(mmodule).has(mclass.intro)
+	end
+
 	init(mclass: MClass, rank: Int)
 	do
 		self.mclass = mclass
@@ -1023,7 +1374,6 @@ class MParameterType
 end
 
 # A type prefixed with "nullable"
-# FIXME Stub implementation
 class MNullableType
 	super MType
 
@@ -1035,18 +1385,29 @@ class MNullableType
 	init(mtype: MType)
 	do
 		self.mtype = mtype
+		self.to_s = "nullable {mtype}"
 	end
 
-	redef fun to_s do return "nullable {mtype}"
+	redef var to_s: String
 
 	redef fun need_anchor do return mtype.need_anchor
 	redef fun as_nullable do return self
+	redef fun as_notnullable do return mtype
 	redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 	do
 		var res = self.mtype.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 		return res.as_nullable
 	end
 
+	redef fun can_resolve_for(mtype, anchor, mmodule)
+	do
+		return self.mtype.can_resolve_for(mtype, anchor, mmodule)
+	end
+
+	redef fun depth do return self.mtype.depth
+
+	redef fun length do return self.mtype.length
+
 	redef fun collect_mclassdefs(mmodule)
 	do
 		assert not self.need_anchor
@@ -1068,7 +1429,7 @@ end
 
 # The type of the only value null
 #
-# The is only one null type per model, see `MModel::null_type'.
+# The is only one null type per model, see `MModel::null_type`.
 class MNullType
 	super MType
 	redef var model: Model
@@ -1080,6 +1441,7 @@ class MNullType
 	redef fun as_nullable do return self
 	redef fun need_anchor do return false
 	redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual) do return self
+	redef fun can_resolve_for(mtype, anchor, mmodule) do return true
 
 	redef fun collect_mclassdefs(mmodule) do return new HashSet[MClassDef]
 
@@ -1088,18 +1450,39 @@ class MNullType
 	redef fun collect_mtypes(mmodule) do return new HashSet[MClassType]
 end
 
-# A signature of a method (or a closure)
+# A signature of a method
 class MSignature
 	super MType
 
 	# The each parameter (in order)
 	var mparameters: Array[MParameter]
 
-	var mclosures = new Array[MParameter]
-
 	# The return type (null for a procedure)
 	var return_mtype: nullable MType
 
+	redef fun depth
+	do
+		var dmax = 0
+		var t = self.return_mtype
+		if t != null then dmax = t.depth
+		for p in mparameters do
+			var d = p.mtype.depth
+			if d > dmax then dmax = d
+		end
+		return dmax + 1
+	end
+
+	redef fun length
+	do
+		var res = 1
+		var t = self.return_mtype
+		if t != null then res += t.length
+		for p in mparameters do
+			res += p.mtype.length
+		end
+		return res
+	end
+
 	# REQUIRE: 1 <= mparameters.count p -> p.is_vararg
 	init(mparameters: Array[MParameter], return_mtype: nullable MType)
 	do
@@ -1116,7 +1499,7 @@ class MSignature
 		self.vararg_rank = vararg_rank
 	end
 
-	# The rank of the ellipsis (...) for vararg (starting from 0).
+	# The rank of the ellipsis (`...`) for vararg (starting from 0).
 	# value is -1 if there is no vararg.
 	# Example: for "(a: Int, b: Bool..., c: Char)" #-> vararg_rank=1
 	var vararg_rank: Int
@@ -1126,7 +1509,7 @@ class MSignature
 
 	redef fun to_s
 	do
-		var b = new Buffer
+		var b = new FlatBuffer
 		if not mparameters.is_empty then
 			b.append("(")
 			for i in [0..mparameters.length[ do
@@ -1149,7 +1532,7 @@ class MSignature
 		return b.to_s
 	end
 
-	redef fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MSignature
+	redef fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MSignature
 	do
 		var params = new Array[MParameter]
 		for p in self.mparameters do
@@ -1160,17 +1543,16 @@ class MSignature
 			ret = ret.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 		end
 		var res = new MSignature(params, ret)
-		for p in self.mclosures do
-			res.mclosures.add(p.resolve_for(mtype, anchor, mmodule, cleanup_virtual))
-		end
 		return res
 	end
 end
 
 # A parameter in a signature
 class MParameter
+	super MEntity
+
 	# The name of the parameter
-	var name: String
+	redef var name: String
 
 	# The static type of the parameter
 	var mtype: MType
@@ -1178,27 +1560,46 @@ class MParameter
 	# Is the parameter a vararg?
 	var is_vararg: Bool
 
-	fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MParameter
+	init(name: String, mtype: MType, is_vararg: Bool) do
+		self.name = name
+		self.mtype = mtype
+		self.is_vararg = is_vararg
+	end
+
+	redef fun to_s
+	do
+		if is_vararg then
+			return "{name}: {mtype}..."
+		else
+			return "{name}: {mtype}"
+		end
+	end
+
+	fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MParameter
 	do
 		if not self.mtype.need_anchor then return self
 		var newtype = self.mtype.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
 		var res = new MParameter(self.name, newtype, self.is_vararg)
 		return res
 	end
+
+	redef fun model do return mtype.model
 end
 
 # A service (global property) that generalize method, attribute, etc.
 #
-# MProperty are global to the model; it means that a MProperty is not bound
+# `MProperty` are global to the model; it means that a `MProperty` is not bound
 # to a specific `MModule` nor a specific `MClass`.
 #
-# A MProperty gather definitions (see `mpropdefs') ; one for the introduction
+# A MProperty gather definitions (see `mpropdefs`) ; one for the introduction
 # and the other in subclasses and in refinements.
 #
-# A MProperty is used to denotes services in polymorphic way (ie. independent
+# A `MProperty` is used to denotes services in polymorphic way (ie. independent
 # of any dynamic type).
-# For instance, a call site "x.foo" is associated to a MProperty.
+# For instance, a call site "x.foo" is associated to a `MProperty`.
 abstract class MProperty
+	super MEntity
+
 	# The associated MPropDef subclass.
 	# The two specialization hierarchy are symmetric.
 	type MPROPDEF: MPropDef
@@ -1209,7 +1610,7 @@ abstract class MProperty
 	var intro_mclassdef: MClassDef
 
 	# The (short) name of the property
-	var name: String
+	redef var name: String
 
 	# The canonical name of the property
 	# Example: "owner::my_module::MyClass::my_method"
@@ -1238,12 +1639,14 @@ abstract class MProperty
 	var mpropdefs: Array[MPROPDEF] = new Array[MPROPDEF]
 
 	# The definition that introduced the property
-	# Warning: the introduction is the first `MPropDef' object
+	# Warning: the introduction is the first `MPropDef` object
 	# associated to self. If self is just created without having any
 	# associated definition, this method will abort
 	fun intro: MPROPDEF do return mpropdefs.first
 
-	# Alias for `name'
+	redef fun model do return intro.model
+
+	# Alias for `name`
 	redef fun to_s do return name
 
 	# Return the most specific property definitions defined or inherited by a type.
@@ -1255,7 +1658,7 @@ abstract class MProperty
 	fun lookup_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
 	do
 		assert not mtype.need_anchor
-		if mtype isa MNullableType then mtype = mtype.mtype
+		mtype = mtype.as_notnullable
 
 		var cache = self.lookup_definitions_cache[mmodule, mtype]
 		if cache != null then return cache
@@ -1278,37 +1681,7 @@ abstract class MProperty
 		end
 
 		# Second, filter the most specific ones
-		var res = new Array[MPROPDEF]
-		for pd1 in candidates do
-			var cd1 = pd1.mclassdef
-			var c1 = cd1.mclass
-			var keep = true
-			for pd2 in candidates do
-				if pd2 == pd1 then continue # do not compare with self!
-				var cd2 = pd2.mclassdef
-				var c2 = cd2.mclass
-				if c2.mclass_type == c1.mclass_type then
-					if cd2.mmodule.in_importation <= cd1.mmodule then
-						# cd2 refines cd1; therefore we skip pd1
-						keep = false
-						break
-					end
-				else if cd2.bound_mtype.is_subtype(mmodule, null, cd1.bound_mtype) then
-					# cd2 < cd1; therefore we skip pd1
-					keep = false
-					break
-				end
-			end
-			if keep then
-				res.add(pd1)
-			end
-		end
-		if res.is_empty then
-			print "All lost! {candidates.join(", ")}"
-			# FIXME: should be abort!
-		end
-		self.lookup_definitions_cache[mmodule, mtype] = res
-		return res
+		return select_most_specific(mmodule, candidates)
 	end
 
 	private var lookup_definitions_cache: HashMap2[MModule, MType, Array[MPROPDEF]] = new HashMap2[MModule, MType, Array[MPROPDEF]]
@@ -1320,14 +1693,14 @@ abstract class MProperty
 	#
 	# If you want the really most specific property, then look at `lookup_next_definition`
 	#
-	# FIXME: Move to MPropDef?
-	fun lookup_super_definitions(mmodule: MModule, mtype: MType): Array[MPropDef]
+	# FIXME: Move to `MPropDef`?
+	fun lookup_super_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
 	do
 		assert not mtype.need_anchor
-		if mtype isa MNullableType then mtype = mtype.mtype
+		mtype = mtype.as_notnullable
 
 		# First, select all candidates
-		var candidates = new Array[MPropDef]
+		var candidates = new Array[MPROPDEF]
 		for mpropdef in self.mpropdefs do
 			# If the definition is not imported by the module, then skip
 			if not mmodule.in_importation <= mpropdef.mclassdef.mmodule then continue
@@ -1342,7 +1715,14 @@ abstract class MProperty
 		if candidates.length <= 1 then return candidates
 
 		# Second, filter the most specific ones
-		var res = new Array[MPropDef]
+		return select_most_specific(mmodule, candidates)
+	end
+
+	# Return an array containing olny the most specific property definitions
+	# This is an helper function for `lookup_definitions` and `lookup_super_definitions`
+	private fun select_most_specific(mmodule: MModule, candidates: Array[MPROPDEF]): Array[MPROPDEF]
+	do
+		var res = new Array[MPROPDEF]
 		for pd1 in candidates do
 			var cd1 = pd1.mclassdef
 			var c1 = cd1.mclass
@@ -1352,12 +1732,12 @@ abstract class MProperty
 				var cd2 = pd2.mclassdef
 				var c2 = cd2.mclass
 				if c2.mclass_type == c1.mclass_type then
-					if cd2.mmodule.in_importation <= cd1.mmodule then
+					if cd2.mmodule.in_importation < cd1.mmodule then
 						# cd2 refines cd1; therefore we skip pd1
 						keep = false
 						break
 					end
-				else if cd2.bound_mtype.is_subtype(mmodule, null, cd1.bound_mtype) then
+				else if cd2.bound_mtype.is_subtype(mmodule, null, cd1.bound_mtype) and cd2.bound_mtype != cd1.bound_mtype then
 					# cd2 < cd1; therefore we skip pd1
 					keep = false
 					break
@@ -1375,19 +1755,54 @@ abstract class MProperty
 	end
 
 	# Return the most specific definition in the linearization of `mtype`.
-	# If mtype does not know mproperty then null is returned.
 	#
 	# If you want to know the next properties in the linearization,
 	# look at `MPropDef::lookup_next_definition`.
 	#
-	# FIXME: NOT YET IMPLEMENTED
+	# FIXME: the linearisation is still unspecified
 	#
-	# REQUIRE: not mtype.need_anchor
-	fun lookup_first_definition(mmodule: MModule, mtype: MType): nullable MPROPDEF
+	# REQUIRE: `not mtype.need_anchor`
+	# REQUIRE: `mtype.has_mproperty(mmodule, self)`
+	fun lookup_first_definition(mmodule: MModule, mtype: MType): MPROPDEF
+	do
+		assert mtype.has_mproperty(mmodule, self)
+		return lookup_all_definitions(mmodule, mtype).first
+	end
+
+	# Return all definitions in a linearisation order
+	# Most speficic first, most general last
+	fun lookup_all_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
 	do
 		assert not mtype.need_anchor
-		return null
+		mtype = mtype.as_notnullable
+
+		var cache = self.lookup_all_definitions_cache[mmodule, mtype]
+		if cache != null then return cache
+
+		#print "select prop {mproperty} for {mtype} in {self}"
+		# First, select all candidates
+		var candidates = new Array[MPROPDEF]
+		for mpropdef in self.mpropdefs do
+			# If the definition is not imported by the module, then skip
+			if not mmodule.in_importation <= mpropdef.mclassdef.mmodule then continue
+			# If the definition is not inherited by the type, then skip
+			if not mtype.is_subtype(mmodule, null, mpropdef.mclassdef.bound_mtype) then continue
+			# Else, we keep it
+			candidates.add(mpropdef)
+		end
+		# Fast track for only one candidate
+		if candidates.length <= 1 then
+			self.lookup_all_definitions_cache[mmodule, mtype] = candidates
+			return candidates
+		end
+
+		mmodule.linearize_mpropdefs(candidates)
+		candidates = candidates.reversed
+		self.lookup_all_definitions_cache[mmodule, mtype] = candidates
+		return candidates
 	end
+
+	private var lookup_all_definitions_cache: HashMap2[MModule, MType, Array[MPROPDEF]] = new HashMap2[MModule, MType, Array[MPROPDEF]]
 end
 
 # A global method
@@ -1401,11 +1816,18 @@ class MMethod
 		super
 	end
 
+	# Is the property defined at the top_level of the module?
+	# Currently such a property are stored in `Object`
+	var is_toplevel: Bool writable = false
+
 	# Is the property a constructor?
 	# Warning, this property can be inherited by subclasses with or without being a constructor
-	# therefore, you should use `is_init_for' the verify if the property is a legal constructor for a given class
+	# therefore, you should use `is_init_for` the verify if the property is a legal constructor for a given class
 	var is_init: Bool writable = false
 
+	# The constructor is a (the) root init with empty signature but a set of initializers
+	var is_root_init: Bool writable = false
+
 	# The the property a 'new' contructor?
 	var is_new: Bool writable = false
 
@@ -1447,11 +1869,12 @@ end
 
 # A definition of a property (local property)
 #
-# Unlike MProperty, a MPropDef is a local definition that belong to a
+# Unlike `MProperty`, a `MPropDef` is a local definition that belong to a
 # specific class definition (which belong to a specific module)
 abstract class MPropDef
+	super MEntity
 
-	# The associated MProperty subclass.
+	# The associated `MProperty` subclass.
 	# the two specialization hierarchy are symmetric
 	type MPROPERTY: MProperty
 
@@ -1474,30 +1897,37 @@ abstract class MPropDef
 		self.location = location
 		mclassdef.mpropdefs.add(self)
 		mproperty.mpropdefs.add(self)
+		self.to_s = "{mclassdef}#{mproperty}"
 	end
 
+	# Actually the name of the `mproperty`
+	redef fun name do return mproperty.name
+
+	redef fun model do return mclassdef.model
+
 	# Internal name combining the module, the class and the property
 	# Example: "mymodule#MyClass#mymethod"
-	redef fun to_s
-	do
-		return "{mclassdef}#{mproperty}"
-	end
+	redef var to_s: String
 
 	# Is self the definition that introduce the property?
 	fun is_intro: Bool do return mproperty.intro == self
 
 	# Return the next definition in linearization of `mtype`.
-	# If there is no next method then null is returned.
 	#
 	# This method is used to determine what method is called by a super.
 	#
-	# FIXME: NOT YET IMPLEMENTED
-	#
-	# REQUIRE: not mtype.need_anchor
-	fun lookup_next_definition(mmodule: MModule, mtype: MType): nullable MPROPDEF
+	# REQUIRE: `not mtype.need_anchor`
+	fun lookup_next_definition(mmodule: MModule, mtype: MType): MPROPDEF
 	do
 		assert not mtype.need_anchor
-		return null
+
+		var mpropdefs = self.mproperty.lookup_all_definitions(mmodule, mtype)
+		var i = mpropdefs.iterator
+		while i.is_ok and i.item != self do i.next
+		assert has_property: i.is_ok
+		i.next
+		assert has_next_property: i.is_ok
+		return i.item
 	end
 end
 
@@ -1515,6 +1945,28 @@ class MMethodDef
 
 	# The signature attached to the property definition
 	var msignature: nullable MSignature writable = null
+
+	# The signature attached to the `new` call on a root-init
+	# This is a concatenation of the signatures of the initializers
+	#
+	# REQUIRE `mproperty.is_root_init == (new_msignature != null)`
+	var new_msignature: nullable MSignature writable = null
+
+	# List of initialisers to call in root-inits
+	#
+	# They could be setters or attributes
+	#
+	# REQUIRE `mproperty.is_root_init == (new_msignature != null)`
+	var initializers = new Array[MProperty]
+
+	# Is the method definition abstract?
+	var is_abstract: Bool writable = false
+
+	# Is the method definition intern?
+	var is_intern writable = false
+
+	# Is the method definition extern?
+	var is_extern writable = false
 end
 
 # A local definition of an attribute
@@ -1547,15 +1999,18 @@ class MVirtualTypeDef
 
 	# The bound of the virtual type
 	var bound: nullable MType writable = null
+
+	# Is the bound fixed?
+	var is_fixed writable = false
 end
 
 # A kind of class.
 #
-#  * abstract_kind
-#  * concrete_kind
-#  * interface_kind
-#  * enum_kind
-#  * extern_kind
+#  * `abstract_kind`
+#  * `concrete_kind`
+#  * `interface_kind`
+#  * `enum_kind`
+#  * `extern_kind`
 #
 # Note this class is basically an enum.
 # FIXME: use a real enum once user-defined enums are available
@@ -1569,10 +2024,28 @@ class MClassKind
 		self.to_s = s
 		self.need_init = need_init
 	end
+
+	# Can a class of kind `self` specializes a class of kine `other`?
+	fun can_specialize(other: MClassKind): Bool
+	do
+		if other == interface_kind then return true # everybody can specialize interfaces
+		if self == interface_kind or self == enum_kind then
+			# no other case for interfaces
+			return false
+		else if self == extern_kind then
+			# only compatible with themselve
+			return self == other
+		else if other == enum_kind or other == extern_kind then
+			# abstract_kind and concrete_kind are incompatible
+			return false
+		end
+		# remain only abstract_kind and concrete_kind
+		return true
+	end
 end
 
 fun abstract_kind: MClassKind do return once new MClassKind("abstract class", true)
 fun concrete_kind: MClassKind do return once new MClassKind("class", true)
 fun interface_kind: MClassKind do return once new MClassKind("interface", false)
 fun enum_kind: MClassKind do return once new MClassKind("enum", false)
-fun extern_kind: MClassKind do return once new MClassKind("extern", false)
+fun extern_kind: MClassKind do return once new MClassKind("extern class", false)