Skip to content
  • Richard Eisenberg's avatar
    Fix #17405 by not checking imported equations · 55ca1085
    Richard Eisenberg authored and Marge Bot's avatar Marge Bot committed
    Previously, we checked all imported type family equations
    for injectivity. This is very silly. Now, we check only
    for conflicts.
    
    Before I could even imagine doing the fix, I needed to untangle
    several functions that were (in my opinion) overly complicated.
    It's still not quite as perfect as I'd like, but it's good enough
    for now.
    
    Test case: typecheck/should_compile/T17405
    55ca1085