src/model: remove extra } from `MGenericType::to_s`
[nit.git] / src / model / model.nit
index 3d6440b..b483543 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
-       var mclasses: Array[MClass] = new Array[MClass]
+       var mclasses = new Array[MClass]
 
        # All known properties
-       var mproperties: Array[MProperty] = new Array[MProperty]
+       var mproperties = new Array[MProperty]
 
        # Hierarchy of class definition.
        #
        # Each classdef is associated with its super-classdefs in regard to
        # its module of definition.
-       var mclassdef_hierarchy: POSet[MClassDef] = new POSet[MClassDef]
+       var mclassdef_hierarchy = new POSet[MClassDef]
 
        # Class-type hierarchy restricted to the introduction.
        #
@@ -55,7 +52,7 @@ redef class Model
        # This poset will evolve in a monotonous way:
        # * Two non connected nodes will remain unconnected
        # * New nodes can appear with new edges
-       private var intro_mtype_specialization_hierarchy: POSet[MClassType] = new POSet[MClassType]
+       private var intro_mtype_specialization_hierarchy = new POSet[MClassType]
 
        # Global overlapped class-type hierarchy.
        # The hierarchy when all modules are combined.
@@ -64,12 +61,12 @@ redef class Model
        # This poset will evolve in an anarchic way. Loops can even be created.
        #
        # FIXME decide what to do on loops
-       private var full_mtype_specialization_hierarchy: POSet[MClassType] = new POSet[MClassType]
+       private var full_mtype_specialization_hierarchy = new POSet[MClassType]
 
        # Collections of classes grouped by their short name
-       private var mclasses_by_name: MultiHashMap[String, MClass] = new MultiHashMap[String, MClass]
+       private var mclasses_by_name = 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)
@@ -77,17 +74,13 @@ redef class Model
        # Visibility or modules are not considered
        fun get_mclasses_by_name(name: String): nullable Array[MClass]
        do
-               if mclasses_by_name.has_key(name) then
-                       return mclasses_by_name[name]
-               else
-                       return null
-               end
+               return mclasses_by_name.get_or_null(name)
        end
 
        # Collections of properties grouped by their short name
-       private var mproperties_by_name: MultiHashMap[String, MProperty] = new MultiHashMap[String, MProperty]
+       private var mproperties_by_name = 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)
@@ -95,26 +88,51 @@ redef class Model
        # Visibility or modules are not considered
        fun get_mproperties_by_name(name: String): nullable Array[MProperty]
        do
-               if not mproperties_by_name.has_key(name) then
-                       return null
-               else
-                       return mproperties_by_name[name]
-               end
+               return mproperties_by_name.get_or_null(name)
        end
 
        # The only null type
-       var null_type: MNullType = new MNullType(self)
+       var null_type = 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
        # All the classes introduced in the module
-       var intro_mclasses: Array[MClass] = new Array[MClass]
+       var intro_mclasses = new Array[MClass]
 
        # All the class definitions of the module
        # (introduction and refinement)
-       var mclassdefs: Array[MClassDef] = new Array[MClassDef]
+       var mclassdefs = 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 +157,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,14 +167,14 @@ redef class MModule
                return res
        end
 
-       # Sort a given array of classes using the linerarization order of the module
+       # Sort a given array of classes using the linearization 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
+       # Sort a given array of class definitions using the linearization 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])
@@ -164,7 +183,7 @@ redef class MModule
                sorter.sort(mclassdefs)
        end
 
-       # Sort a given array of property definitions using the linerarization order of the module
+       # Sort a given array of property definitions using the linearization 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])
@@ -175,7 +194,7 @@ redef class MModule
 
        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
@@ -187,7 +206,10 @@ redef class MModule
 
        private var object_type_cache: nullable MClassType
 
-       # The primitive type Bool
+       # The type `Pointer`, super class to all extern classes
+       var pointer_type: MClassType = self.get_primitive_class("Pointer").mclass_type is lazy
+
+       # The primitive type `Bool`
        fun bool_type: MClassType
        do
                var res = self.bool_type_cache
@@ -199,7 +221,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")
@@ -207,37 +229,59 @@ redef class MModule
                return get_primitive_class("Sys").mclass_type
        end
 
-       # Force to get the primitive class named `name' or abort
+       # The primitive type `Finalizable`
+       # Used to tag classes that need to be finalized.
+       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)
                if cla == null then
-                       if name == "Bool" then
-                               var c = new MClass(self, name, 0, enum_kind, public_visibility)
-                               var cladef = new MClassDef(self, c.mclass_type, new Location(null, 0,0,0,0), new Array[String])
+                       if name == "Bool" and self.model.get_mclasses_by_name("Object") != null then
+                               # Bool is injected because it is needed by engine to code the result
+                               # of the implicit casts.
+                               var c = new MClass(self, name, null, enum_kind, public_visibility)
+                               var cladef = new MClassDef(self, c.mclass_type, new Location(null, 0,0,0,0))
+                               cladef.set_supertypes([object_type])
+                               cladef.add_in_hierarchy
                                return c
                        end
                        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
@@ -245,7 +289,8 @@ redef class MModule
 end
 
 private class MClassDefSorter
-       super AbstractSorter[MClassDef]
+       super Comparator
+       redef type COMPARED: MClassDef
        var mmodule: MModule
        redef fun compare(a, b)
        do
@@ -257,7 +302,8 @@ private class MClassDefSorter
 end
 
 private class MPropDefSorter
-       super AbstractSorter[MPropDef]
+       super Comparator
+       redef type COMPARED: MPropDef
        var mmodule: MModule
        redef fun compare(pa, pb)
        do
@@ -272,15 +318,28 @@ 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
@@ -288,74 +347,89 @@ 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"
-       fun full_name: String
-       do
-               return "{self.intro_mmodule.full_name}::{name}"
+       #
+       # It is the name of the class prefixed by the full_name of the `intro_mmodule`
+       # Example: `"owner::module::MyClass"`
+       redef var full_name is lazy do
+               return "{self.intro_mmodule.namespace_for(visibility)}::{name}"
+       end
+
+       redef var c_name is lazy do
+               return "{intro_mmodule.c_namespace_for(visibility)}__{name.to_cmangle}"
        end
 
        # The number of generic formal parameters
        # 0 if the class is not generic
-       var arity: Int
+       var arity: Int is noinit
 
-       # The kind of the class (interface, abstract class, etc.)
-       # In Nit, the kind of a class cannot evolve in refinements
-       var kind: MClassKind
-
-       # The visibility of the class
-       # In Nit, the visibility of a class cannot evolve in refinements
-       var visibility: MVisibility
+       # Each generic formal parameters in order.
+       # is empty if the class is not generic
+       var mparameters = new Array[MParameterType]
 
-       init(intro_mmodule: MModule, name: String, arity: Int, kind: MClassKind, visibility: MVisibility)
+       # Initialize `mparameters` from their names.
+       protected fun setup_parameter_names(parameter_names: nullable Array[String]) is
+               autoinit
        do
-               self.intro_mmodule = intro_mmodule
-               self.name = name
-               self.arity = arity
-               self.kind = kind
-               self.visibility = visibility
-               intro_mmodule.intro_mclasses.add(self)
-               var model = intro_mmodule.model
-               model.mclasses_by_name.add_one(name, self)
-               model.mclasses.add(self)
+               if parameter_names == null then
+                       self.arity = 0
+               else
+                       self.arity = parameter_names.length
+               end
 
                # Create the formal parameter types
                if arity > 0 then
+                       assert parameter_names != null
                        var mparametertypes = new Array[MParameterType]
                        for i in [0..arity[ do
-                               var mparametertype = new MParameterType(self, i)
+                               var mparametertype = new MParameterType(self, i, parameter_names[i])
                                mparametertypes.add(mparametertype)
                        end
+                       self.mparameters = mparametertypes
                        var mclass_type = new MGenericType(self, mparametertypes)
                        self.mclass_type = mclass_type
-                       self.get_mtype_cache.add(mclass_type)
+                       self.get_mtype_cache[mparametertypes] = mclass_type
                else
                        self.mclass_type = new MClassType(self)
                end
        end
 
-       # All class definitions (introduction and refinements)
-       var mclassdefs: Array[MClassDef] = new Array[MClassDef]
+       # The kind of the class (interface, abstract class, etc.)
+       # In Nit, the kind of a class cannot evolve in refinements
+       var kind: MClassKind
 
-       # Alias for `name'
-       redef fun to_s do return self.name
+       # The visibility of the class
+       # In Nit, the visibility of a class cannot evolve in refinements
+       var visibility: MVisibility
 
-       # The definition that introduced the class
-       # 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
+       init
        do
-               assert has_a_first_definition: not mclassdefs.is_empty
-               return mclassdefs.first
+               intro_mmodule.intro_mclasses.add(self)
+               var model = intro_mmodule.model
+               model.mclasses_by_name.add_one(name, self)
+               model.mclasses.add(self)
        end
 
-       # Return the class `self' in the class hierarchy of the module `mmodule'.
+       redef fun model do return intro_mmodule.model
+
+       # All class definitions (introduction and refinements)
+       var mclassdefs = new Array[MClassDef]
+
+       # Alias for `name`
+       redef fun to_s do return self.name
+
+       # The definition that introduces the class.
        #
-       # SEE: MModule::flatten_mclass_hierarchy
-       # REQUIRE: mmodule.has_mclass(self)
+       # Warning: such a definition may not exist in the early life of the object.
+       # In this case, the method will abort.
+       var intro: MClassDef is noinit
+
+       # 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]
@@ -363,97 +437,140 @@ 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
-       var mclass_type: MClassType
+       # ENSURE: `mclass_type.mclass == self`
+       var mclass_type: MClassType is noinit
 
        # 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
                if self.arity == 0 then return self.mclass_type
-               for t in self.get_mtype_cache do
-                       if t.arguments == mtype_arguments then
-                               return t
-                       end
-               end
-               var res = new MGenericType(self, mtype_arguments)
-               self.get_mtype_cache.add res
+               var res = get_mtype_cache.get_or_null(mtype_arguments)
+               if res != null then return res
+               res = new MGenericType(self, mtype_arguments)
+               self.get_mtype_cache[mtype_arguments.to_a] = res
                return res
        end
 
-       private var get_mtype_cache: Array[MGenericType] = new Array[MGenericType]
+       private var get_mtype_cache = new HashMap[Array[MType], MGenericType]
 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
-       var mclass: MClass
+       # The associated `MClass`
+       var mclass: MClass is noinit
 
        # 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)
-       var parameter_names: Array[String]
-
        # The origin of the definition
        var location: Location
 
        # Internal name combining the module and the class
        # Example: "mymodule#MyClass"
-       redef fun to_s do return "{mmodule}#{mclass}"
+       redef var to_s: String is noinit
 
-       init(mmodule: MModule, bound_mtype: MClassType, location: Location, parameter_names: Array[String])
+       init
        do
-               assert bound_mtype.mclass.arity == parameter_names.length
-               self.bound_mtype = bound_mtype
-               self.mmodule = mmodule
                self.mclass = bound_mtype.mclass
-               self.location = location
                mmodule.mclassdefs.add(self)
                mclass.mclassdefs.add(self)
-               self.parameter_names = parameter_names
+               if mclass.intro_mmodule == mmodule then
+                       assert not isset mclass._intro
+                       mclass.intro = self
+               end
+               self.to_s = "{mmodule}#{mclass}"
+       end
+
+       # Actually the name of the `mclass`
+       redef fun name do return mclass.name
+
+       # The module and class name separated by a '#'.
+       #
+       # The short-name of the class is used for introduction.
+       # Example: "my_module#MyClass"
+       #
+       # The full-name of the class is used for refinement.
+       # Example: "my_module#intro_module::MyClass"
+       redef var full_name is lazy do
+               if is_intro then
+                       # public gives 'p#A'
+                       # private gives 'p::m#A'
+                       return "{mmodule.namespace_for(mclass.visibility)}#{mclass.name}"
+               else if mclass.intro_mmodule.mproject != mmodule.mproject then
+                       # public gives 'q::n#p::A'
+                       # private gives 'q::n#p::m::A'
+                       return "{mmodule.full_name}#{mclass.full_name}"
+               else if mclass.visibility > private_visibility then
+                       # public gives 'p::n#A'
+                       return "{mmodule.full_name}#{mclass.name}"
+               else
+                       # private gives 'p::n#::m::A' (redundant p is omitted)
+                       return "{mmodule.full_name}#::{mclass.intro_mmodule.name}::{mclass.name}"
+               end
+       end
+
+       redef var c_name is lazy do
+               if is_intro then
+                       return "{mmodule.c_namespace_for(mclass.visibility)}___{mclass.c_name}"
+               else if mclass.intro_mmodule.mproject == mmodule.mproject and mclass.visibility > private_visibility then
+                       return "{mmodule.c_name}___{mclass.name.to_cmangle}"
+               else
+                       return "{mmodule.c_name}___{mclass.c_name}"
+               end
        end
 
+       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]
+       var supertypes = new Array[MClassType]
 
        # 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
@@ -477,8 +594,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
@@ -494,27 +611,27 @@ 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`?
        fun is_intro: Bool do return mclass.intro == self
 
        # All properties introduced by the classdef
-       var intro_mproperties: Array[MProperty] = new Array[MProperty]
+       var intro_mproperties = new Array[MProperty]
 
        # All property definitions in the class (introductions and redefinitions)
-       var mpropdefs: Array[MPropDef] = new Array[MPropDef]
+       var mpropdefs = new Array[MPropDef]
 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
@@ -526,48 +643,40 @@ 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
                if sub == sup then return true
+
+               #print "1.is {sub} a {sup}? ===="
+
                if anchor == null then
                        assert not sub.need_anchor
                        assert not sup.need_anchor
-               end
-
-               # 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.mclass.mclass_type, anchor, mmodule, false)
-               end
-               if sup isa MParameterType or sup isa MVirtualType then
-                       assert anchor != null
-                       sup = sup.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, false)
+               else
+                       # First, resolve the formal types to the simplest equivalent forms in the receiver
+                       assert sub.can_resolve_for(anchor, null, mmodule)
+                       sub = sub.lookup_fixed(mmodule, anchor)
+                       assert sup.can_resolve_for(anchor, null, mmodule)
+                       sup = sup.lookup_fixed(mmodule, anchor)
                end
 
                # Does `sup` accept null or not?
@@ -591,15 +700,17 @@ abstract class MType
                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
+               while sub isa MParameterType or sub isa MVirtualType do
+                       #print "3.is {sub} a {sup}?"
+
+                       # A unfixed formal type can only accept itself
+                       if sub == sup then return true
+
                        assert anchor != null
-                       sub = sub.anchor_to(mmodule, anchor)
+                       sub = sub.lookup_bound(mmodule, anchor)
+
+                       #print "3.is {sub} a {sup}?"
 
                        # Manage the second layer of null/nullable
                        if sub isa MNullableType then
@@ -609,9 +720,15 @@ abstract class MType
                                return sup_accept_null
                        end
                end
+               #print "4.is {sub} a {sup}? <- no more resolution"
 
                assert sub isa MClassType # It is the only remaining type
 
+               # A unfixed formal type can only accept itself
+               if sup isa MParameterType or sup isa MVirtualType then
+                       return false
+               end
+
                if sup isa MNullType then
                        # `sup` accepts only null
                        return false
@@ -651,34 +768,40 @@ 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.
@@ -686,17 +809,28 @@ 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]
+       #
+       # ~~~nitish
+       #     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
@@ -707,51 +841,132 @@ 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
-       #     end
-       #     class B super A[Int] end
+       # ## 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
        #
-       # FIXME: the parameter `cleanup_virtual' is just a bad idea, but having
+       # ~~~nitish
+       # class A[E]
+       #     fun foo(e:E):E is abstract
+       # end
+       # class C[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(C[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]],C[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
+
+       # Resolve formal type to its verbatim bound.
+       # If the type is not formal, just return self
+       #
+       # The result is returned exactly as declared in the "type" property (verbatim).
+       # So it could be another formal type.
+       #
+       # In case of conflict, the method aborts.
+       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType do return self
+
+       # Resolve the formal type to its simplest equivalent form.
+       #
+       # Formal types are either free or fixed.
+       # When it is fixed, it means that it is equivalent with a simpler type.
+       # When a formal type is free, it means that it is only equivalent with itself.
+       # This method return the most simple equivalent type of `self`.
+       #
+       # This method is mainly used for subtype test in order to sanely compare fixed.
+       #
+       # By default, return self.
+       # See the redefinitions for specific behavior in each kind of type.
+       fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType do return self
+
+       # 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
+       #
+       # ~~~nitish
+       # 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
@@ -761,15 +976,25 @@ 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 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.
+       # The depth of the type seen as a tree.
        #
-       # A -> 1
-       # G[A] -> 2
-       # H[A, B] -> 2
-       # H[G[A], B] -> 3
+       # * A -> 1
+       # * G[A] -> 2
+       # * H[A, B] -> 2
+       # * H[G[A], B] -> 3
        #
        # Formal types have a depth of 1.
        fun depth: Int
@@ -777,6 +1002,19 @@ abstract class MType
                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
@@ -784,26 +1022,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
@@ -813,7 +1051,7 @@ end
 
 # A type based on a class.
 #
-# MClassType have properties (see `has_property').
+# `MClassType` have properties (see `has_mproperty`).
 class MClassType
        super MType
 
@@ -822,17 +1060,18 @@ class MClassType
 
        redef fun model do return self.mclass.intro_mmodule.model
 
-       private init(mclass: MClass)
-       do
-               self.mclass = mclass
-       end
+       # TODO: private init because strongly bounded to its mclass. see `mclass.mclass_type`
 
        # The formal arguments of the type
-       # ENSURE: return.length == self.mclass.arity
-       var arguments: Array[MType] = new Array[MType]
+       # ENSURE: `result.length == self.mclass.arity`
+       var arguments = new Array[MType]
 
        redef fun to_s do return mclass.to_s
 
+       redef fun full_name do return mclass.full_name
+
+       redef fun c_name do return mclass.c_name
+
        redef fun need_anchor do return false
 
        redef fun anchor_to(mmodule: MModule, anchor: MClassType): MClassType
@@ -840,7 +1079,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
@@ -854,14 +1095,21 @@ class MClassType
 
        redef fun collect_mclasses(mmodule)
        do
+               if collect_mclasses_last_module == mmodule then return collect_mclasses_last_module_cache
                assert not self.need_anchor
                var cache = self.collect_mclasses_cache
                if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
-               return cache[mmodule]
+               var res = cache[mmodule]
+               collect_mclasses_last_module = mmodule
+               collect_mclasses_last_module_cache = res
+               return res
        end
 
+       private var collect_mclasses_last_module: nullable MModule = null
+       private var collect_mclasses_last_module_cache: Set[MClass] is noinit
+
        redef fun collect_mtypes(mmodule)
        do
                assert not self.need_anchor
@@ -872,7 +1120,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]
@@ -902,9 +1150,9 @@ class MClassType
                collect_mtypes_cache[mmodule] = types
        end
 
-       private var collect_mclassdefs_cache: HashMap[MModule, Set[MClassDef]] = new HashMap[MModule, Set[MClassDef]]
-       private var collect_mclasses_cache: HashMap[MModule, Set[MClass]] = new HashMap[MModule, Set[MClass]]
-       private var collect_mtypes_cache: HashMap[MModule, Set[MClassType]] = new HashMap[MModule, Set[MClassType]]
+       private var collect_mclassdefs_cache = new HashMap[MModule, Set[MClassDef]]
+       private var collect_mclasses_cache = new HashMap[MModule, Set[MClass]]
+       private var collect_mtypes_cache = new HashMap[MModule, Set[MClassType]]
 
 end
 
@@ -913,11 +1161,13 @@ end
 class MGenericType
        super MClassType
 
-       private init(mclass: MClass, arguments: Array[MType])
+       redef var arguments
+
+       # TODO: private init because strongly bounded to its mclass. see `mclass.get_mtype`
+
+       init
        do
-               super(mclass)
                assert self.mclass.arity == arguments.length
-               self.arguments = arguments
 
                self.need_anchor = false
                for t in arguments do
@@ -926,20 +1176,40 @@ 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(", ")}]"
+       # The short-name of the class, then the full-name of each type arguments within brackets.
+       # Example: `"Map[String, List[Int]]"`
+       redef var to_s: String is noinit
+
+       # The full-name of the class, then the full-name of each type arguments within brackets.
+       # Example: `"standard::Map[standard::String, standard::List[standard::Int]]"`
+       redef var full_name is lazy do
+               var args = new Array[String]
+               for t in arguments do
+                       args.add t.full_name
+               end
+               return "{mclass.full_name}[{args.join(", ")}]"
        end
 
-       redef var need_anchor: Bool
+       redef var c_name is lazy do
+               var res = mclass.c_name
+               # Note: because the arity is known, a prefix notation is enough
+               for t in arguments do
+                       res += "__"
+                       res += t.c_name
+               end
+               return res.to_s
+       end
+
+       redef var need_anchor: Bool is noinit
 
        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))
@@ -947,6 +1217,16 @@ class MGenericType
                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
@@ -956,6 +1236,15 @@ class MGenericType
                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.
@@ -964,99 +1253,129 @@ class MVirtualType
 
        # The property associated with the type.
        # Its the definitions of this property that determine the bound or the virtual type.
-       var mproperty: MProperty
+       var mproperty: MVirtualTypeProp
 
        redef fun model do return self.mproperty.intro_mclassdef.mmodule.model
 
-       # Lookup the bound for a given resolved_receiver
-       # The result may be a other virtual type (or a parameter type)
-       #
-       # The result is returned exactly as declared in the "type" property (verbatim).
-       #
-       # In case of conflict, the method aborts.
-       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       do
+               return lookup_single_definition(mmodule, resolved_receiver).bound.as(not null)
+       end
+
+       private fun lookup_single_definition(mmodule: MModule, resolved_receiver: MType): MVirtualTypeDef
        do
                assert not resolved_receiver.need_anchor
                var props = self.mproperty.lookup_definitions(mmodule, resolved_receiver)
                if props.is_empty then
                        abort
                else if props.length == 1 then
-                       return props.first.as(MVirtualTypeDef).bound.as(not null)
+                       return props.first
                end
                var types = new ArraySet[MType]
+               var res  = props.first
                for p in props do
-                       types.add(p.as(MVirtualTypeDef).bound.as(not null))
+                       types.add(p.bound.as(not null))
+                       if not res.is_fixed then res = p
                end
                if types.length == 1 then
-                       return types.first
+                       return res
                end
                abort
        end
 
+       # A VT is fixed when:
+       # * the VT is (re-)defined with the annotation `is fixed`
+       # * the VT is (indirectly) bound to an enum class (see `enum_kind`) since there is no subtype possible
+       # * the receiver is an enum class since there is no subtype possible
+       redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
+       do
+               assert not resolved_receiver.need_anchor
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
+
+               var prop = lookup_single_definition(mmodule, resolved_receiver)
+               var res = prop.bound.as(not null)
+
+               # Recursively lookup the fixed result
+               res = res.lookup_fixed(mmodule, resolved_receiver)
+
+               # 1. For a fixed VT, return the resolved bound
+               if prop.is_fixed then return res
+
+               # 2. For a enum boud, return the bound
+               if res isa MClassType and res.mclass.kind == enum_kind then return res
+
+               # 3. for a enum receiver return the bound
+               if resolved_receiver.mclass.kind == enum_kind then return res
+
+               return self
+       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_receiver
+               if mtype.need_anchor then
+                       assert anchor != null
+                       resolved_receiver = mtype.resolve_for(anchor, null, mmodule, true)
+               else
+                       resolved_receiver = mtype
+               end
                # Now, we can get the bound
-               var verbatim_bound = lookup_bound(mmodule, resolved_reciever)
+               var verbatim_bound = lookup_bound(mmodule, resolved_receiver)
                # 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, cleanup_virtual)
-               #print "{class_name}: {self}/{mtype}/{anchor} -> {self}/{resolved_reciever}/{anchor} -> {verbatim_bound}/{mtype}/{anchor} -> {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
-               # 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
+               return res
        end
 
-       redef fun to_s do return self.mproperty.to_s
-
-       init(mproperty: MProperty)
+       redef fun can_resolve_for(mtype, anchor, mmodule)
        do
-               self.mproperty = mproperty
+               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
+
+       redef fun full_name do return self.mproperty.full_name
+
+       redef fun c_name do return self.mproperty.c_name
 end
 
-# The type associated the a formal parameter generic type of a class
+# The type associated to a formal parameter generic type of a class
 #
 # Each parameter type is associated to a specific class.
-# It's mean that all refinements of a same class "share" the parameter type,
-# but that a generic subclass has its on parameter types.
+# It means that all refinements of a same class "share" the parameter type,
+# but that a generic subclass has its own 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.
 #
 # Example:
+#
 #     class A[E]
 #         fun e: E is abstract
 #     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).
 class MParameterType
        super MType
 
@@ -1066,22 +1385,26 @@ 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
-       # Names of parameter types changes in each class definition
-       # Therefore, this method return an internal name.
-       # Example: return "G#1" for the second parameter of the class G
-       # FIXME: add a way to get the real name in a classdef
-       redef fun to_s do return "{mclass}#{rank}"
+       redef var name
+
+       redef fun to_s do return name
 
-       # Resolve the bound for a given resolved_receiver
-       # The result may be a other virtual type (or a parameter type)
-       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       redef var full_name is lazy do return "{mclass.full_name}::{name}"
+
+       redef var c_name is lazy do return mclass.c_name + "__" + "#{name}".to_cmangle
+
+       redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
                var goalclass = self.mclass
+               if resolved_receiver.mclass == goalclass then
+                       return resolved_receiver.arguments[self.rank]
+               end
                var supertypes = resolved_receiver.collect_mtypes(mmodule)
                for t in supertypes do
                        if t.mclass == goalclass then
@@ -1094,26 +1417,55 @@ class MParameterType
                abort
        end
 
+       # A PT is fixed when:
+       # * Its bound is a enum class (see `enum_kind`).
+       #   The PT is just useless, but it is still a case.
+       # * More usually, the `resolved_receiver` is a subclass of `self.mclass`,
+       #   so it is necessarily fixed in a `super` clause, either with a normal type
+       #   or with another PT.
+       #   See `resolve_for` for examples about related issues.
+       redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
+       do
+               assert not resolved_receiver.need_anchor
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
+               var res = self.resolve_for(resolved_receiver.mclass.mclass_type, resolved_receiver, mmodule, false)
+               return res
+       end
+
        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)
+               # FIXME: What happens here is far from clear. Thus this part must be validated and clarified
+               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 # It is the only remaining type
 
                # Eh! The parameter is in the current class.
                # So we return the corresponding argument, no mater what!
@@ -1123,7 +1475,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
@@ -1134,15 +1489,17 @@ class MParameterType
                return res
        end
 
-       init(mclass: MClass, rank: Int)
+       redef fun can_resolve_for(mtype, anchor, mmodule)
        do
-               self.mclass = mclass
-               self.rank = rank
+               if mtype.need_anchor then
+                       assert anchor != null
+                       mtype = mtype.anchor_to(mmodule, anchor)
+               end
+               return mtype.collect_mclassdefs(mmodule).has(mclass.intro)
        end
 end
 
 # A type prefixed with "nullable"
-# FIXME Stub implementation
 class MNullableType
        super MType
 
@@ -1151,23 +1508,43 @@ class MNullableType
 
        redef fun model do return self.mtype.model
 
-       init(mtype: MType)
+       init
        do
-               self.mtype = mtype
+               self.to_s = "nullable {mtype}"
        end
 
-       redef fun to_s do return "nullable {mtype}"
+       redef var to_s: String is noinit
+
+       redef var full_name is lazy do return "nullable {mtype.full_name}"
+
+       redef var c_name is lazy do return "nullable__{mtype.c_name}"
 
        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
+
+       # Efficiently returns `mtype.lookup_fixed(mmodule, resolved_receiver).as_nullable`
+       redef fun lookup_fixed(mmodule, resolved_receiver)
+       do
+               var t = mtype.lookup_fixed(mmodule, resolved_receiver)
+               if t == mtype then return self
+               return t.as_nullable
+       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
@@ -1189,18 +1566,17 @@ 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
-       protected init(model: Model)
-       do
-               self.model = model
-       end
        redef fun to_s do return "null"
+       redef fun full_name do return "null"
+       redef fun c_name do return "null"
        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]
 
@@ -1209,15 +1585,13 @@ 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
 
@@ -1230,15 +1604,22 @@ class MSignature
                        var d = p.mtype.depth
                        if d > dmax then dmax = d
                end
-               for p in mclosures 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)
+       init
        do
                var vararg_rank = -1
                for i in [0..mparameters.length[ do
@@ -1248,22 +1629,20 @@ class MSignature
                                vararg_rank = i
                        end
                end
-               self.mparameters = mparameters
-               self.return_mtype = return_mtype
                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
+       var vararg_rank: Int is noinit
 
        # The number or parameters
        fun arity: Int do return mparameters.length
 
        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
@@ -1286,7 +1665,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
@@ -1297,17 +1676,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
@@ -1315,27 +1693,42 @@ class MParameter
        # Is the parameter a vararg?
        var is_vararg: Bool
 
-       fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MParameter
+       redef fun to_s
+       do
+               if is_vararg then
+                       return "{name}: {mtype}..."
+               else
+                       return "{name}: {mtype}"
+               end
+       end
+
+       # Returns a new parameter with the `mtype` resolved.
+       # See `MType::resolve_for` for details.
+       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
@@ -1346,23 +1739,29 @@ 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"
-       fun full_name: String
-       do
-               return "{self.intro_mclassdef.mmodule.full_name}::{self.intro_mclassdef.mclass.name}::{name}"
+       # The canonical name of the property.
+       #
+       # It is the short-`name` prefixed by the short-name of the class and the full-name of the module.
+       # Example: "my_project::my_module::MyClass::my_method"
+       redef var full_name is lazy do
+               return "{intro_mclassdef.mmodule.namespace_for(visibility)}::{intro_mclassdef.mclass.name}::{name}"
+       end
+
+       redef var c_name is lazy do
+               # FIXME use `namespace_for`
+               return "{intro_mclassdef.mmodule.c_name}__{intro_mclassdef.mclass.name.to_cmangle}__{name.to_cmangle}"
        end
 
        # The visibility of the property
        var visibility: MVisibility
 
-       init(intro_mclassdef: MClassDef, name: String, visibility: MVisibility)
+       # Is the property usable as an initializer?
+       var is_autoinit = false is writable
+
+       init
        do
-               self.intro_mclassdef = intro_mclassdef
-               self.name = name
-               self.visibility = visibility
                intro_mclassdef.intro_mproperties.add(self)
                var model = intro_mclassdef.mmodule.model
                model.mproperties_by_name.add_one(name, self)
@@ -1372,15 +1771,17 @@ abstract class MProperty
        # All definitions of the property.
        # The first is the introduction,
        # The other are redefinitions (in refinements and in subclasses)
-       var mpropdefs: Array[MPROPDEF] = new Array[MPROPDEF]
+       var mpropdefs = new Array[MPROPDEF]
+
+       # The definition that introduces the property.
+       #
+       # Warning: such a definition may not exist in the early life of the object.
+       # In this case, the method will abort.
+       var intro: MPROPDEF is noinit
 
-       # The definition that introduced the property
-       # 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
+       redef fun model do return intro.model
 
-       # Alias for `name'
+       # Alias for `name`
        redef fun to_s do return name
 
        # Return the most specific property definitions defined or inherited by a type.
@@ -1389,10 +1790,13 @@ abstract class MProperty
        # If mtype does not know mproperty then an empty array is returned.
        #
        # If you want the really most specific property, then look at `lookup_first_definition`
+       #
+       # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
+       # ENSURE: `not mtype.has_mproperty(mmodule, self) == result.is_empty`
        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
@@ -1415,40 +1819,10 @@ 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]]
+       private var lookup_definitions_cache = new HashMap2[MModule, MType, Array[MPROPDEF]]
 
        # Return the most specific property definitions inherited by a type.
        # The selection knows that refinement is stronger than specialization;
@@ -1457,14 +1831,15 @@ 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]
+       # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
+       # ENSURE: `not mtype.has_mproperty(mmodule, self) implies result.is_empty`
+       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
@@ -1479,7 +1854,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
@@ -1489,12 +1871,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
@@ -1516,25 +1898,30 @@ abstract class MProperty
        # If you want to know the next properties in the linearization,
        # look at `MPropDef::lookup_next_definition`.
        #
-       # FIXME: the linearisation is still unspecified
+       # FIXME: the linearization is still unspecified
        #
-       # REQUIRE: not mtype.need_anchor
-       # REQUIRE: mtype.has_mproperty(mmodule, self)
+       # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
+       # REQUIRE: `mtype.has_mproperty(mmodule, self)`
        fun lookup_first_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                return lookup_all_definitions(mmodule, mtype).first
        end
 
-       # Return all definitions in a linearisation order
-       # Most speficic first, most general last
+       # Return all definitions in a linearization order
+       # Most specific first, most general last
+       #
+       # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
+       # REQUIRE: `mtype.has_mproperty(mmodule, self)`
        fun lookup_all_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_all_definitions_cache[mmodule, mtype]
                if cache != null then return cache
 
+               assert not mtype.need_anchor
+               assert mtype.has_mproperty(mmodule, self)
+
                #print "select prop {mproperty} for {mtype} in {self}"
                # First, select all candidates
                var candidates = new Array[MPROPDEF]
@@ -1558,7 +1945,7 @@ abstract class MProperty
                return candidates
        end
 
-       private var lookup_all_definitions_cache: HashMap2[MModule, MType, Array[MPROPDEF]] = new HashMap2[MModule, MType, Array[MPROPDEF]]
+       private var lookup_all_definitions_cache = new HashMap2[MModule, MType, Array[MPROPDEF]]
 end
 
 # A global method
@@ -1567,18 +1954,20 @@ class MMethod
 
        redef type MPROPDEF: MMethodDef
 
-       init(intro_mclassdef: MClassDef, name: String, visibility: MVisibility)
-       do
-               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
+       # Is the property a 'new' constructor?
+       var is_new: Bool = false is writable
 
        # Is the property a legal constructor for a given class?
        # As usual, visibility is not considered.
@@ -1595,10 +1984,6 @@ class MAttribute
 
        redef type MPROPDEF: MAttributeDef
 
-       init(intro_mclassdef: MClassDef, name: String, visibility: MVisibility)
-       do
-               super
-       end
 end
 
 # A global virtual type
@@ -1607,52 +1992,121 @@ class MVirtualTypeProp
 
        redef type MPROPDEF: MVirtualTypeDef
 
-       init(intro_mclassdef: MClassDef, name: String, visibility: MVisibility)
-       do
-               super
-       end
-
        # The formal type associated to the virtual type property
-       var mvirtualtype: MVirtualType = new MVirtualType(self)
+       var mvirtualtype = new MVirtualType(self)
 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
 
        # Self class
        type MPROPDEF: MPropDef
 
-       # The origin of the definition
-       var location: Location
-
        # The class definition where the property definition is
        var mclassdef: MClassDef
 
        # The associated global property
        var mproperty: MPROPERTY
 
-       init(mclassdef: MClassDef, mproperty: MPROPERTY, location: Location)
+       # The origin of the definition
+       var location: Location
+
+       init
        do
-               self.mclassdef = mclassdef
-               self.mproperty = mproperty
-               self.location = location
                mclassdef.mpropdefs.add(self)
                mproperty.mpropdefs.add(self)
+               if mproperty.intro_mclassdef == mclassdef then
+                       assert not isset mproperty._intro
+                       mproperty.intro = self
+               end
+               self.to_s = "{mclassdef}#{mproperty}"
        end
 
+       # Actually the name of the `mproperty`
+       redef fun name do return mproperty.name
+
+       # The full-name of mpropdefs combine the information about the `classdef` and the `mproperty`.
+       #
+       # Therefore the combination of identifiers is awful,
+       # the worst case being
+       #
+       #  * a property "p::m::A::x"
+       #  * redefined in a refinement of a class "q::n::B"
+       #  * in a module "r::o"
+       #  * so "r::o#q::n::B#p::m::A::x"
+       #
+       # Fortunately, the full-name is simplified when entities are repeated.
+       # For the previous case, the simplest form is "p#A#x".
+       redef var full_name is lazy do
+               var res = new FlatBuffer
+
+               # The first part is the mclassdef. Worst case is "r::o#q::n::B"
+               res.append mclassdef.full_name
+
+               res.append "#"
+
+               if mclassdef.mclass == mproperty.intro_mclassdef.mclass then
+                       # intro are unambiguous in a class
+                       res.append name
+               else
+                       # Just try to simplify each part
+                       if mclassdef.mmodule.mproject != mproperty.intro_mclassdef.mmodule.mproject then
+                               # precise "p::m" only if "p" != "r"
+                               res.append mproperty.intro_mclassdef.mmodule.full_name
+                               res.append "::"
+                       else if mproperty.visibility <= private_visibility then
+                               # Same project ("p"=="q"), but private visibility,
+                               # does the module part ("::m") need to be displayed
+                               if mclassdef.mmodule.namespace_for(mclassdef.mclass.visibility) != mproperty.intro_mclassdef.mmodule.mproject then
+                                       res.append "::"
+                                       res.append mproperty.intro_mclassdef.mmodule.name
+                                       res.append "::"
+                               end
+                       end
+                       if mclassdef.mclass != mproperty.intro_mclassdef.mclass then
+                               # precise "B" only if not the same class than "A"
+                               res.append mproperty.intro_mclassdef.name
+                               res.append "::"
+                       end
+                       # Always use the property name "x"
+                       res.append mproperty.name
+               end
+               return res.to_s
+       end
+
+       redef var c_name is lazy do
+               var res = new FlatBuffer
+               res.append mclassdef.c_name
+               res.append "___"
+               if mclassdef.mclass == mproperty.intro_mclassdef.mclass then
+                       res.append name.to_cmangle
+               else
+                       if mclassdef.mmodule != mproperty.intro_mclassdef.mmodule then
+                               res.append mproperty.intro_mclassdef.mmodule.c_name
+                               res.append "__"
+                       end
+                       if mclassdef.mclass != mproperty.intro_mclassdef.mclass then
+                               res.append mproperty.intro_mclassdef.name.to_cmangle
+                               res.append "__"
+                       end
+                       res.append mproperty.name.to_cmangle
+               end
+               return res.to_s
+       end
+
+       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 noinit
 
        # Is self the definition that introduce the property?
        fun is_intro: Bool do return mproperty.intro == self
@@ -1661,9 +2115,7 @@ abstract class MPropDef
        #
        # This method is used to determine what method is called by a super.
        #
-       # FIXME: IMPLEMENTED AS A static designation, it is ugly
-       #
-       # REQUIRE: not mtype.need_anchor
+       # REQUIRE: `not mtype.need_anchor`
        fun lookup_next_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                assert not mtype.need_anchor
@@ -1685,13 +2137,40 @@ class MMethodDef
        redef type MPROPERTY: MMethod
        redef type MPROPDEF: MMethodDef
 
-       init(mclassdef: MClassDef, mproperty: MPROPERTY, location: Location)
-       do
-               super
-       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
+
+       # An optional constant value returned in functions.
+       #
+       # Only some specific primitife value are accepted by engines.
+       # Is used when there is no better implementation available.
+       #
+       # Currently used only for the implementation of the `--define`
+       # command-line option.
+       # SEE: module `mixin`.
+       var constant_value: nullable Object = null is writable
 end
 
 # A local definition of an attribute
@@ -1701,13 +2180,8 @@ class MAttributeDef
        redef type MPROPERTY: MAttribute
        redef type MPROPDEF: MAttributeDef
 
-       init(mclassdef: MClassDef, mproperty: MPROPERTY, location: Location)
-       do
-               super
-       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
@@ -1717,22 +2191,20 @@ class MVirtualTypeDef
        redef type MPROPERTY: MVirtualTypeProp
        redef type MPROPDEF: MVirtualTypeDef
 
-       init(mclassdef: MClassDef, mproperty: MPROPERTY, location: Location)
-       do
-               super
-       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
@@ -1741,15 +2213,35 @@ class MClassKind
 
        # Is a constructor required?
        var need_init: Bool
-       private init(s: String, need_init: Bool)
+
+       # TODO: private init because enumeration.
+
+       # Can a class of kind `self` specializes a class of kine `other`?
+       fun can_specialize(other: MClassKind): Bool
        do
-               self.to_s = s
-               self.need_init = need_init
+               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 themselves
+                       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
 
+# The class kind `abstract`
 fun abstract_kind: MClassKind do return once new MClassKind("abstract class", true)
+# The class kind `concrete`
 fun concrete_kind: MClassKind do return once new MClassKind("class", true)
+# The class kind `interface`
 fun interface_kind: MClassKind do return once new MClassKind("interface", false)
+# The class kind `enum`
 fun enum_kind: MClassKind do return once new MClassKind("enum", false)
-fun extern_kind: MClassKind do return once new MClassKind("extern", false)
+# The class kind `extern`
+fun extern_kind: MClassKind do return once new MClassKind("extern class", false)