Skip to content
  • Richard Eisenberg's avatar
    Warn on inferred polymorphic recursion · 2d1b9619
    Richard Eisenberg authored and Marge Bot's avatar Marge Bot committed
    Silly users sometimes try to use visible dependent quantification
    and polymorphic recursion without a CUSK or SAK. This causes
    unexpected errors. So we now adjust expectations with a bit
    of helpful messaging.
    
    Closes #17541 and closes #17131.
    
    test cases: dependent/should_fail/T{17541{,b},17131}
    2d1b9619