Make NoExtCon fields strict

added TTG label

Hooray

Is there anything really to review? I saw your updated comments in the TTG note and am happy with them.

Actually, there is one mildly unsatisfying aspect of this MR that I'd like your input on. It takes some digging to find, but there are actually parts of the MR where I added lines of code rather than deleting them. Here is one example:

 instDeclDataFamInsts inst_decls
   = concatMap do_one inst_decls
   where
+    do_one :: LInstDecl (GhcPass p) -> [DataFamInstDecl (GhcPass p)]
     do_one (L _ (ClsInstD { cid_inst = ClsInstDecl { cid_datafam_insts = fam_insts } }))
       = map unLoc fam_insts
     do_one (L _ (DataFamInstD { dfid_inst = fam_inst }))      = [fam_inst]
     do_one (L _ (TyFamInstD {}))                              = []
-    do_one (L _ (ClsInstD _ (XClsInstDecl nec))) = noExtCon nec
-    do_one (L _ (XInstDecl nec))                 = noExtCon nec

You might wonder why I added a type signature to do_one. It turns out that if you omit the type signature, then GHC won't warn that the XClsInstDecl and XInstDecl cases are inaccessible! I found this somewhat annoying, since GHC didn't warn me about it on my first attempt at drafting this MR; I only discovered it post facto by grep'ing for remaining uses of noExtCon. I dug into this a bit and minimized the phenomenon down to a bite-sized example:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Foo where

data NoExtCon
noExtCon :: NoExtCon -> a
noExtCon x = case x of {}

data GhcPass pass
type family XX a
type instance XX (GhcPass _) = NoExtCon

data HsThing p
  = MkHsThing ()
  | XHsThing !(XX p)

f :: HsThing (GhcPass p) -> ()
f (MkHsThing x) = x
f (XHsThing  v) = noExtCon v

g :: HsThing (GhcPass p) -> ()
g = h
  where
    h (MkHsThing x) = x
    h (XHsThing  v) = noExtCon v

Of the two functions f and g, only f will warn that the match on XHsThing is inaccessible. Why does g not warn, then? After some digging, it turns out that the inferred type of h is (XX p ~ NoExtCon) => HsThing p -> (). That's a bit strange, but things get even stranger from here. h only infers this type if there is at least one instance for XX defined! If you comment out the type instance XX (GhcPass _) = NoExtCon line, then h will fail to typecheck altogether:

Foo.hs:23:5: error:
    • Couldn't match type ‘XX (GhcPass p)’ with ‘NoExtCon’
        arising from a use of ‘h’
    • In the expression: h
      In an equation for ‘g’:
          g = h
            where
                h (MkHsThing x) = x
                h (XHsThing v) = noExtCon v
    • Relevant bindings include
        g :: HsThing (GhcPass p) -> () (bound at Foo.hs:23:1)
   |
23 | g = h
   |     ^

I have two questions:

Why wouldn't h's inferred type be HsThing (GhcPass p) -> ()?
Assuming that inferring (XX p ~ NoExtCon) => HsThing p -> () is the correct behavior, why would type inference succeed or fail depending on the presence of type instance XX (GhcPass _) = NoExtCon? Shouldn't GHC infer (XX p ~ NoExtCon) regardless of the instances in scope due to the open world assumption?

added pattern match warnings label

Adding @sgraf812

Could you possibly extend https://gitlab.haskell.org/ghc/ghc/-/wikis/implementing-trees-that-grow/trees-that-grow-guidance to describe the noExtCon idiom specifically; and to explain about the strictness of the constructor extension field, which you are carefully adding here?

I made a section for it, with a bit to fill in. Thanks!

Could you possibly extend https://gitlab.haskell.org/ghc/ghc/-/wikis/implementing-trees-that-grow/trees-that-grow-guidance to describe the noExtCon idiom specifically; and to explain about the strictness of the constructor extension field, which you are carefully adding here?

I'm not sure what you mean by "the noExtCon idiom". There is no such idiom, since this MR removes it! :)

In all seriousness, I know what you mean. I've updated the wiki page with some prose about the use of strict fields in extension constructors.

... and I'll add @matheus23 who might be interested in following this.

In all seriousness, I know what you mean. I've updated the wiki page with some prose about the use of strict fields in extension constructors.

Ah! I see. I've updated it some more. See if you agree. To avoid distraction I've used error rather than noExtCon. It might be worth adding a bit about the noExtCon idiom for the few places where it (for some reason) remains (if it does).

If you comment out the type instance XX (GhcPass _) = NoExtCon line, then h will fail to typecheck altogether:

That is not surprising. Consider

    h (XHsThing  v) = noExtCon v

Now noExtCon requires an arg of type NoExtCon. But v :: XX (GhcPass p). Hence type error.

After some digging, it turns out that the inferred type of h is (XX p ~ NoExtCon) => HsThing p -> (). That's a bit strange

For the reasoning see Note [Quantifying over equality constraints] in TcType. It's a bit of a heuristic, to be sure, but I don't know how to do better.

Ah! I see. I've updated it some more. See if you agree.

LGTM.

For the reasoning see Note [Quantifying over equality constraints] in TcType. It's a bit of a heuristic, to be sure, but I don't know how to do better.

Ah, I was wondering if there was a special case for quantifying over equality constraints when type families are involved like this. It turns out that is indeed the case! Thanks, that thoroughly answers question (1) from !3005 (comment 262496).

As for question (2)...

(2) makes sense though, because it still infers XX p ~ NoExtCon and ultimately fails to satisfy that constraint seeing that p is GhcPass. Note that it doesn't fail to type-check h, it fails to type-check g.

Oops, very good point. I had overlooked that h does infer the correct type, but it is too general for g. In fact, there's nothing particularly interesting about the fact that h is a local function. You could just as well lift it to the top level:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Foo where

data NoExtCon
noExtCon :: NoExtCon -> a
noExtCon x = case x of {}

data GhcPass pass
type family XX a

data HsThing p
  = MkHsThing ()
  | XHsThing !(XX p)

h (MkHsThing x) = x
h (XHsThing  v) = noExtCon v

Here, h will infer the type (XX p ~ NoExtCon) => HsThing p -> (), even without any XX type family instances defined. This aligns with how I would expect this to behave, so this answers question (2) nicely.

All of my questions have been answered, so I think this MR is good to go. Any other review comments before assigning this to @marge-bot?

approved this merge request

Actually, there is one thing that needs to be done before merging this: I need to land haddock@bc3bf19c into the ghc-head branch (otherwise, @marge-bot will be unhappy). However, I can't just do so right now: the tip of the ghc-head branch currently has commit haddock@163da780, which only validates assuming you have applied the changes from !2924 (closed) in GHC itself. These changes are not yet in GHC's master, however.

In short, I think it would be simplest to momentarily park this MR until !2924 (closed) lands in master.

mentioned in merge request !2924 (closed)

added 32 commits

6ae1e0f5...255418da - 31 commits from branch master
04b6cf94 - Make NoExtCon fields strict

Compare with previous version

resolved all threads

Make NoExtCon fields strict

Merge request reports

Activity