[#854] Make WithDeMorganScope instances more principled

Description

Make WithDeMorganScope instances more principled, avoiding a non-compiler-checked "impossible" error.

Related issue(s)

Retain type information for a bit longer to let GHC check our work in withDeMorganScope instances.

Resolves #854 (closed)

Checklist for your Merge Request

Related changes (conditional)

• Tests (see short guidelines)

  • If I added new functionality, I added tests covering it.
  • If I fixed a bug, I added a regression test to prevent the bug from silently reappearing again.

• Documentation

  • I checked whether I should update the docs and did so if necessary:
    • Root README and other README.md files
    • Haddock
    • docs/
  • I updated changelog files of all affected packages released to Hackage if my changes are externally visible.

Stylistic guide (mandatory)

• My commits comply with the following policy.
• My code complies with the style guide.

added 1 commit

• 330d102f - [#854 (closed)] Make WithDeMorganScope instances more principled

Compare with previous version

changed title from [#854 (closed)] Make WithDeMorgan instances more principled to [#854 (closed)] Make WithDeMorganScope instances more principled

changed the description

marked the checklist item My code complies with the style guide. as completed

marked the checklist item My commits comply with the following policy. as completed

marked the checklist item I updated changelog files of all affected packages released to Hackage if my changes are externally visible. as completed

marked the checklist item Root README and other README.md files as completed

marked the checklist item Haddock as completed

marked the checklist item docs/ as completed

marked the checklist item If I fixed a bug, I added a regression test to prevent the bug from as completed

marked the checklist item If I added new functionality, I added tests covering it. as completed

This change is not externally visible. How do I satisfy the CI bot without a changelog entry?

approved this merge request

requested review from @pasqu4le and @lierdakil

Let's take HasNoOp t as an example. We have an instance if ContainsOp t ~ 'False -- which we can conjure into existence from thin air with unsafeCoerce. For it to be safe, we need to be sure that ContainsOp t indeed evaluates to False, but that will be verified by the inefficient code. And the efficient code essentially boils down to

unsafeWithDeMorganScope f =
  case (unsafeCoerce Refl :: ContainsOp t :~: 'False) of
    Refl -> f

which we can generalize using type applications to accept the family we need to unsafeCoerce as a parameter. Which we can then directly use in rule definitions. So, one ambiguous polymorphic helper function and one rule per instance with explicit type binders.

I'm sure there are some gotchas, but at first glance this seems workable?

If we're going to do something unsafe, I'd prefer to keep the trusted base as small as possible, as in OrL and OrR. So I'm imagining maybe a singletons-like defunctionalization of the type families so we can talk about ideas like "The passed type family works like this when passed this sort of structure with these substructures".

"Unsafe" is a relative term here. As long as GHC actually uses the "inefficient but verifiable" implementation to typecheck everything and then substitutes the appropriate "unsafe" one, the "unsafe" one is as safe as the "inefficient" one. One possible gotcha I see here is a mistake in rewriting rules would end up in a segfault. But that's something we'll have to make peace with regardless.

changed this line in version 3 of the diff

As I expected, I was able to get it down to one, pretty much legitimate, rule. The process of figuring out how to go from two rules to one had the side benefit of pointing out how to go from two SingI constraints in each instance down to one, which is kind of neat.

@lierdakil The test failure in https://gitlab.com/morley-framework/morley/-/jobs/2898171237 is very troubling. I can't imagine that this change has anything to do with it; is there something known to be fragile or did we just hit a lucky test case and discover a problem?

added 1 commit

• f97d3071 - [#854 (closed)] Make WithDeMorganScope instances more principled

Compare with previous version

added 1 commit

• 372bf978 - fixup! [#854 (closed)] Make WithDeMorganScope instances more principled

Compare with previous version

marked this merge request as draft from 372bf978

added 1 commit

• 1dad23e5 - [#854 (closed)] Make WithDeMorganScope instances more principled

Compare with previous version