Skip to content

Improve injectivity checking

Richard Eisenberg requested to merge rae/ghc:t16512 into master

Commit message:

    Implement a coverage checker for injectivity
    
    This fixes #16512.
    
    There are lots of parts of this patch:
    
    * The main payload is in FamInst. See
    Note [Coverage condition for injective type families] there
    for the overview. But it doesn't fix the bug.
    
    * We now bump the reduction depth every time we decompose a TyConApp
    or AppTy. This actually fixes the bug. See
    Note [Bump depth when decomposing] in TcCanonical.
    
    * Exploration of this revealed a new, easy to maintain invariant
    for CTyEqCans. See Note [Almost function-free] in TcRnTypes.
    
    * We also realized that type inference for injectivity was a
    bit incomplete. This means we exchanged lookupFlattenTyVar for
    rewriteTyVar. See Note [rewriteTyVar] in TcFlatten. The new
    function is monadic while the previous one was pure, necessitating
    some faff in TcInteract. Nothing too bad.
    
    * zonkCt did not maintain invariants on CTyEqCan. This is now
    checked.
    
    * The pure unifier was finding the fixpoint of the returned
    substitution, even when doing one-way matching (in tcUnifyTysWithTFs).
    Fixed now.
    
    Test cases: typecheck/should_fail/T16512{a,b}

This is ready for review.

Merge request reports