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