Skip to content
  • Iavor S. Diatchki's avatar
    Make type-level evaluation work with :kind! · b2fa2d41
    Iavor S. Diatchki authored
    The main change is to add a case to `reduceTyFamApp_maybe` to evaluate
    built-in type constructors (e.g., (+), (*), and friends).
    
    To avoid problems with recursive modules, I moved the definition of
    TcBuiltInSynFamily from `FamInst` to `FamInstEnv`.  I am still not sure if
    this is the right place.
    
    There is also a wibble that it'd be nice to fix:
    
    when we evaluate a built-in type function, using`sfMatchFam`, we get
    a `TcCoercion`.  However, `reduceTyFamApp_maybe` needs a `Corecion`.
    I couldn't find a nice way to convert between the two, so I resorted to
    a bit of hack (marked with `XXX`).
    
    The hack is that we happen to know that the built-in constructors for
    the type-nat functions always return coercions of shape `TcAxiomRuleCo`,
    with no assumptions, so it easy to convert `TcCoercion` to `Coercion`
    in this one case.  This is enough to make things work, but it is clearly
    a cludge.
    b2fa2d41