Skip to content
  • Simon Peyton Jones's avatar
    Major refactoring of CoAxioms · 98a642cf
    Simon Peyton Jones authored
    This patch should have no user-visible effect.  It implements a
    significant internal refactoring of the way that FC axioms are
    handled.  The ultimate goal is to put us in a position to implement
    "pattern-matching axioms".  But the changes here are only does
    refactoring; there is no change in functionality.
    
    Specifically:
    
     * We now treat data/type family instance declarations very,
       very similarly to types class instance declarations:
    
       - Renamed InstEnv.Instance as InstEnv.ClsInst, for symmetry with
         FamInstEnv.FamInst.  This change does affect the GHC API, but
         for the better I think.
    
       - Previously, each family type/data instance declaration gave rise
         to a *TyCon*; typechecking a type/data instance decl produced
         that TyCon.  Now, each type/data instance gives rise to
         a *FamInst*, by direct analogy with each class instance
         declaration giving rise to a ClsInst.
    
       - Just as each ClsInst contains its evidence, a DFunId, so each FamInst
         contains its evidence, a CoAxiom.  See Note [FamInsts and CoAxioms]
         in FamInstEnv.  The CoAxiom is a System-FC thing, and can relate any
         two types, whereas the FamInst relates directly to the Haskell source
         language construct, and always has a function (F tys) on the LHS.
    
       - Just as a DFunId has its own declaration in an interface file, so now
         do CoAxioms (see IfaceSyn.IfaceAxiom).
    
       These changes give rise to almost all the refactoring.
    
     * We used to have a hack whereby a type family instance produced a dummy
       type synonym, thus
          type instance F Int = Bool -> Bool
       translated to
          axiom FInt :: F Int ~ R:FInt
          type R:FInt = Bool -> Bool
       This was always a hack, and now it's gone.  Instead the type instance
       declaration produces a FamInst, whose axiom has kind
          axiom FInt :: F Int ~ Bool -> Bool
       just as you'd expect.
    
     * Newtypes are done just as before; they generate a CoAxiom. These
       CoAxioms are "implicit" (do not generate an IfaceAxiom declaration),
       unlike the ones coming from family instance declarations.  See
       Note [Implicit axioms] in TyCon
    
    On the whole the code gets significantly nicer.  There were consequential
    tidy-ups in the vectoriser, but I think I got them right.
    98a642cf