Changes between Version 39 and Version 40 of TypeFunctions


Ignore:
Timestamp:
Aug 3, 2006 7:39:45 PM (8 years ago)
Author:
chak
Comment:

Type checking indexed types (III)

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions

    v39 v40  
    158158 2. Case expressions scrutinising indexed types eliminate them. 
    159159 
    160 ==== Wrappers for indexed types ==== 
     160==== Wrappers for indexed data types ==== 
    161161 
    162162The wrapper of a data constructor acts as an impedance matcher between the source-level signatures of the constructor and its actual representation; in particular, it evaluates strict arguments and unboxes flattened arguments.  In the case of a constructor for an indexed data type, it additionally has to apply the coercion between the type function representing the source type and its representation as a vanilla data type.  So, for example, if we have (continuing the example from above) 
     
    172172The generation of constructor wrappers is performed by `MkId.mkDataConIds`. 
    173173 
     174==== Case expressions for indexed data types ==== 
     175 
     176When we scrutinise an indexed type in a case expression, we need to first cast it to the vanilla data type representing the family member from which the constructors guarding the alternatives are drawn.  (This implies that we cannot have any case expression mixing constructors from two or more family members.  In fact, if we had that capability, we would have open GADT definitions in the Löh/Hinze sense.) 
     177 
     178So, whether we need to cast the scrutinee of a case expression depends on the constructors appearing in the alternatives, which are type checked by `TcPat.tcConPat`.  This function uses `TcUnify.boxySplitTyConApp` to match the type of the scrutinee against the result type of the data constructor.  In the case of GADTs and indexed types, this is not just a matter of extracting the arguments from the type constructor application, but we need to match against type patterns.  This matching is already conveniently performed by the code for GADTs. 
     179 
     180If the data constructor is from an indexed type, we need to propagate a coercion (to be applied to the scrutinee) outwards.  For this, GHC also already has a mechanism, namely the variant `CoPat` of `HsPat.Pat`.  It enables us to attach a coercion function, of type `HsBinds.ExprCoFun`, to a pattern, which the desugarer will pick up in `Match.matchCoercion` and apply to the match variable of the case expression. 
     181 
     182`ExprCoFun` represents, besides coercions due to type instantiation, also type equality coercions of type `Coercion.Coercion`.  We use them for coercions that are exactly the converse of the coercion used in the wrapper of the data constructor of the current case alternative.  (There is also an equivalent of `CoPat` for expressions, namely `HsCoerce` of `HsExpr.HsExpr`.) 
     183 
    174184=== Type checking associated types === 
    175185