• Richard Eisenberg's avatar
    Implement a coverage checker for injectivity · 1cd3fa29
    Richard Eisenberg authored
    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 discharge
    a CFunEqCan. See Note [Flatten when discharging CFunEqCan]
    in TcInteract.
    
    * 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. It's not worth
    the bother doing so, so we just transmute CTyEqCans to
    CNonCanonicals.
    
    * 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}
    1cd3fa29
TcInteract.hs 106 KB