Avoiding construction of dead dictionaries

[Michael Sperber]

Thanks for thinking about this one!

On Fri, Aug 06 2021, Tom Smeding <x at tomsmeding.com> wrote:

> Would it not be unsound for ghc to elide dictionary construction here?
> After all, the right-hand side might actually be a bottom
> (e.g. undefined) at run-time, in which case the pattern match cannot
> succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code
that evaluates to bottom?  Can that happen?

> I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub
> Dict))) or ignore the argument altogether (i.e. _), dictionary
> construction will be elided.

Thanks for the hint!  ghc gives me this unfortunately, implying that it
agreed with your first comment:

src/ConCat/Category.hs:190:29: error:
    • Could not deduce: Con b arising from a use of ‘r’
      from the context: Con a
        bound by the type signature for:
                   (<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r
        at src/ConCat/Category.hs:189:1-46
    • In the expression: r
      In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r
    • Relevant bindings include
        r :: Con b => r (bound at src/ConCat/Category.hs:190:1)
        (<+) :: (Con b => r) -> (a |- b) -> r
          (bound at src/ConCat/Category.hs:190:3)
    |
190 | r <+ ~(Entail (Sub Dict)) = r
    |                             ^

Other ideas welcome!

-- 
Regards,
Mike