Skip to content

Consider the stage of typeable evidence when checking stage restriction

Matthew Pickering requested to merge wip/t21547 into master

We were considering all Typeable evidence to be "BuiltinInstance"s which meant the stage restriction was going unchecked. In-fact, typeable has evidence and so we need to apply the stage restriction.

This is complicated by the fact we don't generate typeable evidence and the corresponding DFunIds until after typechecking is concluded so we introcue a new InstanceWhat constructor, BuiltinTypeableInstance which records whether the evidence is going to be local or not.

Fixes #21547 (closed)

Merge request reports