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. (cherry picked from commit 6a1d7f97)
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. (cherry picked from commit 6a1d7f97)