wiki:TypeFunctionsStatus

Version 95 (modified by chak, 8 years ago) (diff)

--

Type Functions: Implementation Status

Back to TypeFunctions.

Current:

  • Re-organise the representation of type instances a bit:
    • Currently, FamInst and IfaceFamInst just copy some info from the type instance declarations. Let's change that and let them have rough match signatures. In the case of IfaceFamInst, only the actual type instances continues to hold the full information. IfaceFamInst is just the rough match signature referring to the type instance. Thereby, move the old IfaceFamInst into IFaceFamInstTy. Then, mi_fam_inst gets the type [IfaceFamInst], as the IfaceDecl no longer has a reference to IfaceFamInst, but only to IFaceFamInstTy.
  • Overlap check for data/newtype instances.
    1. Routine that checks two FamInsts for overlap. See comment in FamInst.addLocalFamInst for what is missing.
    2. In M.hi store the names of all modules below (and including M) that contain family instances. Invariant: if M compiles, then none of those modlues have overlaps.
    3. When compiling a new module K, union the sets from direct imports, plus K itself if it has family instances. If that union is a subset of any of the incoming ones, nothing to do! Otherwise, further checking needed.
    4. Further checking can be brute-force or intelligently to minimise the number of checks. Brute-force: Take the FamInsts of all family-instance modules that are in the complement of the intersection of the sets of family-instance modules contained in each imported module and add K if it has imports. Check this whole set using the check from Point (1). Intelligently: Compute the set of all module pairs that have already been checked for overlap (as they both occur in the family-instance module list of any import) and subtract that from the set of all pairs of visible family-instance modules. These are the critical module pairs. Check any pair of instances coming from two different modules in a critical module pair.
  • There really is no reason anymore to disallow family instances where all arguments are type variables. Such instances are rarely useful, but may be when creating stub files or so; so why disallow them. Check that they are working.

Parsing and Renaming

Todo (low-level):

  • Should family declarations be optional with ATs, too? (See comment at patch making kinds optional at toplevel declarations.)

Todo (high-level):

  1. Parse and rename equality constraints in signatures.
  2. Defaults for associated type synonyms. (Having both a kind signature and vanilla synonym is problematic as in RnNames.getLocalDeclBinders its hard to see that not both of them are defining declarations, which leads to a multiple declarations error. Defaults are quite different from vanilla synonyms anyway, as they usually have tyvars on their rhs that do not occur on the lhs.)
  3. Import/export lists:
    • We need to be able to write something like GMapKey(GMap,empty).
    • Export and import of data constructors declarated in data instances. We should be able to use the same syntax for the entity specs as for closed data types, but the meaning is somewhat different.

Done:

  • Parsing and renaming of kind signatures (toplevel and in classes).
  • Parsing and renaming of indexed type declarations (toplevel and in classes).
  • Using new syntax with family and instance on top level.
  • Added -findexed-types switch.
  • Allowing type tag in export lists to list associated types in the sub-binder list of an import/export item for a class.

Type Checking

Todo (low-level):

  • data/newtype instances may not overlap. (Such definitions would always be non-confluent.) We might be able to get away with a lazy check at every place where a value of family type is constructed (i.e., occurences of the datacon wrapper). Such a value may never be an inhabitant of more than one instance declaration. No, we won't get away with this...
  • RHS of a type instance must be a tau type.
  • Check that patterns of type indexes don't contain type functions.
  • We probably need to replicate quite a bit of the infrastructure used to maintain class instances for type instances. In particular, we need to suck all home package instances into a field in the TcGblEnv similar to tcg_inst_env and all external instances in a field in Hsc.ExternalPackageState similar to eps_inst_env.
  • Construct InstInfo for type equation in tcIdxTyInstDecl1.
  • If an associated synonym has a default definition, use that in the instances. In contrast to methods, this cannot be overridden by a specialised definition. (Confluence requires that any specialised version is extensionally the same as the default.)
  • It should be ok to allow newtype instances for data families. (NB: the rhs of a newtype is guaranteed to be a lifted type.) Is this desirable?

Todo (high-level):

  1. Type checking of type functions (and hence, associated type synonyms); forget about iso for the moment.
  2. Type checking in the presence of associated synonym defaults. (Default AT synonyms are only allowed for ATs defined in the same class.)
  3. Type check functional dependencies as type functions.

Done:

  • Kind and type checking of kind signatures.
  • Kind and type checking of instance declarations of indexed types.
  • Wrapper generation and type checking of pattern matching for indexed data and newtypes.

Desugaring

Todo (low-level):

  • Derivings on an associated data type declaration need to be inherited by all definitions of that data type in instances.

Todo (high-level):

  1. Extend interface files to include equality axioms:
    • How do we exactly want to represent type equations in interface files?
      • SPJ pointed out that instances are maintained in InstEnv.InstEnv with different values for the home packages and others. Type instances may have to be maintained in a similar way, as they are also incrementally collected during compiling a program. (We probably include them in the same structure, as they will also be of type InstInfo.)
      • IfaceInst contains the instance declaration information for interfaces.
      Answer: We don't put anything extra into interface files. Instead, we derive the information corresponding toIfaceInst list in ModIface and the Instance list in ModDetails from the interface declarations and type environment, respectively. I.e., it is the type instances that carry the whole payload. Update: We may actually want to put a rough match signature in the iface seperate from the full instance declaration, so we can delay type checking the full instance declaration until we get a rough match. (This makes only sense for type instances, not for data instances, as the latter are loaded when their constructors are mentioned. Well actually, it does make sense for data instances as far as loading them for overlap checking is concerned.)
  1. Desugar type functions and equality constraints.

Done:

  • Representation of family kind signatures as TyCon.TyCons.
  • Extension of Class.Class by associated TyCons.
  • Extension of TyCon.TyCon with a reference to the parent TyCon for data instances.
  • Extension of DataCon.DataCon with instance types for constructors belonging to data instances.
  • Extension of TyCon.TyCon such that the parent of a data instance is paired with a coercion identifying family instance and representation type.
  • For indexed data types, the datacon wrapper uses data instance coercion and pattern matching casts the scrutinee via an ExprCoFn in a CoPat.
  • Imporet and exporting.

Testsuite

Todo:

  • Compile libraries with CoreLint.
  • Convert TyFuns.hs and the various GMaps to tests in the testsuite. SPJ already created testsuite/tests/ghc-regress/indexed-types.