Thanks for thinking about this one! On Fri, Aug 06 2021, Tom Smeding <x...@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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users