Fix #9085.
Inaccessible equations in a closed type family now leads to a warning, not an error. This echoes what happens at the term level.
Please register or sign in to comment
Inaccessible equations in a closed type family now leads to a warning, not an error. This echoes what happens at the term level.