src: transform all old writable in annotations
[nit.git] / src / model / model.nit
index be77b5b..765e601 100644 (file)
 # 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)
@@ -193,54 +252,91 @@ redef class MModule
                                return c
                        end
                        print("Fatal Error: no primitive class {name}")
-                       abort
+                       exit(1)
+               end
+               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
-               assert cla.length == 1 else print cla.join(", ")
                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
 
-       # Force to get the primitive method named `name' on the type `recv' or abort
-       fun force_get_primitive_method(name: String, recv: MType): MMethod
+private class MClassDefSorter
+       super AbstractSorter[MClassDef]
+       var mmodule: MModule
+       redef fun compare(a, b)
        do
-               var res = try_get_primitive_method(name, recv)
-               if res == null then
-                       print("Fatal Error: no primitive property {name} on {recv}")
-                       abort
-               end
-               return res
+               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
@@ -248,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}"
@@ -296,43 +392,54 @@ 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
-       private fun intro: MClassDef
+       fun intro: MClassDef
        do
                assert has_a_first_definition: not mclassdefs.is_empty
                return mclassdefs.first
        end
 
+       # Return the class `self` in the class hierarchy of the module `mmodule`.
+       #
+       # SEE: `MModule::flatten_mclass_hierarchy`
+       # REQUIRE: `mmodule.has_mclass(self)`
+       fun in_hierarchy(mmodule: MModule): POSetElement[MClass]
+       do
+               return mmodule.flatten_mclass_hierarchy[self]
+       end
+
        # 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
@@ -353,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)
@@ -383,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
@@ -395,21 +511,27 @@ 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]
 
-       # Register the super-types for the class (ie "super SomeType")
-       # This function can only invoked once by class
+       # Register some super-types for the class (ie "super SomeType")
+       #
+       # The hierarchy must not already be set
+       # REQUIRE: `self.in_hierarchy == null`
        fun set_supertypes(supertypes: Array[MClassType])
        do
                assert unique_invocation: self.in_hierarchy == null
                var mmodule = self.mmodule
                var model = mmodule.model
-               var res = model.mclassdef_hierarchy.add_node(self)
-               self.in_hierarchy = res
                var mtype = self.bound_mtype
 
                for supertype in supertypes do
@@ -423,12 +545,29 @@ class MClassDef
                        end
                end
 
+       end
+
+       # 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`
+       fun add_in_hierarchy
+       do
+               assert unique_invocation: self.in_hierarchy == null
+               var model = mmodule.model
+               var res = model.mclassdef_hierarchy.add_node(self)
+               self.in_hierarchy = res
+               var mtype = self.bound_mtype
+
+               # Here we need to connect the mclassdef to its pairs in the mclassdef_hierarchy
+               # The simpliest way is to attach it to collect_mclassdefs
                for mclassdef in mtype.collect_mclassdefs(mmodule) do
                        res.poset.add_edge(self, 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`?
@@ -443,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
@@ -460,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
@@ -490,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
 
-               if sup isa MParameterType or sup isa MVirtualType or sup isa MNullType then
+               # 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.
+
+               # 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)
@@ -535,7 +701,6 @@ abstract class MType
                if not sup isa MGenericType then return true
                var sub2 = sub.supertype_to(mmodule, anchor, sup.mclass)
                assert sub2.mclass == sup.mclass
-               assert sub2 isa MGenericType
                for i in [0..sup.mclass.arity[ do
                        var sub_arg = sub2.arguments[i]
                        var sup_arg = sup.arguments[i]
@@ -557,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.
@@ -592,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
@@ -613,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.
        #
-       # FIXME: the parameter `cleanup_virtual' is just a bad idea, but having
+       #   A[Array[F]].anchor_to(B[nullable Object])  #->  A[Array[nullable Object]]
+       #
+       # 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
@@ -667,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
@@ -676,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
@@ -705,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
 
@@ -719,6 +981,10 @@ class MClassType
                self.mclass = mclass
        end
 
+       # The formal arguments of the type
+       # ENSURE: `result.length == self.mclass.arity`
+       var arguments: Array[MType] = new Array[MType]
+
        redef fun to_s do return mclass.to_s
 
        redef fun need_anchor do return false
@@ -728,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
@@ -760,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]
@@ -814,30 +1082,55 @@ class MGenericType
                                break
                        end
                end
-       end
 
-       # The formal arguments of the type
-       # ENSURE: return.length == self.mclass.arity
-       var arguments: Array[MType]
+               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.
@@ -875,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
@@ -905,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.
 #
@@ -917,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
 
@@ -933,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
@@ -954,7 +1294,6 @@ class MParameterType
                        if t.mclass == goalclass then
                                # Yeah! c specialize goalclass with a "super `t'". So the question is what is the argument of f
                                # FIXME: Here, we stop on the first goal. Should we check others and detect inconsistencies?
-                               assert t isa MGenericType
                                var res = t.arguments[self.rank]
                                return res
                        end
@@ -964,35 +1303,50 @@ 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.as(MGenericType).arguments[resolved_receiver.rank]
+                       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!
                if resolved_receiver.mclass == self.mclass then
-                       assert resolved_receiver isa MGenericType
                        var res = resolved_receiver.arguments[self.rank]
                        #print "{class_name}: {self}/{mtype}/{anchor} -> direct {res}"
                        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
@@ -1003,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
@@ -1011,7 +1374,6 @@ class MParameterType
 end
 
 # A type prefixed with "nullable"
-# FIXME Stub implementation
 class MNullableType
        super MType
 
@@ -1023,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
@@ -1056,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
@@ -1068,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]
 
@@ -1076,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
@@ -1104,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
@@ -1114,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
@@ -1137,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
@@ -1148,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
@@ -1166,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
@@ -1197,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"
@@ -1226,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.
@@ -1243,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
@@ -1266,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]]
@@ -1308,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
@@ -1330,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
@@ -1340,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
@@ -1363,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
@@ -1389,13 +1816,20 @@ 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 = false is writable
+
        # 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
-       var is_init: Bool writable = false
+       # therefore, you should use `is_init_for` the verify if the property is a legal constructor for a given class
+       var is_init: Bool = false is writable
+
+       # The constructor is a (the) root init with empty signature but a set of initializers
+       var is_root_init: Bool = false is writable
 
        # The the property a 'new' contructor?
-       var is_new: Bool writable = false
+       var is_new: Bool = false is writable
 
        # Is the property a legal constructor for a given class?
        # As usual, visibility is not considered.
@@ -1435,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
 
@@ -1462,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
 
@@ -1502,7 +1944,29 @@ class MMethodDef
        end
 
        # The signature attached to the property definition
-       var msignature: nullable MSignature writable = null
+       var msignature: nullable MSignature = null is writable
+
+       # 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 = null is writable
+
+       # 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 = false is writable
+
+       # Is the method definition intern?
+       var is_intern = false is writable
+
+       # Is the method definition extern?
+       var is_extern = false is writable
 end
 
 # A local definition of an attribute
@@ -1518,7 +1982,7 @@ class MAttributeDef
        end
 
        # The static type of the attribute
-       var static_mtype: nullable MType writable = null
+       var static_mtype: nullable MType = null is writable
 end
 
 # A local definition of a virtual type
@@ -1534,16 +1998,19 @@ class MVirtualTypeDef
        end
 
        # The bound of the virtual type
-       var bound: nullable MType writable = null
+       var bound: nullable MType = null is writable
+
+       # Is the bound fixed?
+       var is_fixed = false is writable
 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
@@ -1557,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)