Pattern guards sometimes don't promote

[jstolarek]

Running this code:

type family a :- b where a :- b = a - b
$(genDefunSymbols [''(:-)])

$(promoteOnly [d|
  take                   :: Nat -> [a] -> [a]
  take n _      | n <= 0 =  []
  take _ []              =  []
  take n (x:xs)          =  x : take (n-1) xs
 |])

gives errors:

src/Data/Promotion/Prelude/List.hs:236:3:
    Inaccessible family instance equation:
      Case_1627447744 arg_16274464270 arg_16274464290 '(z0, '[]) = '[]
    In the equations for closed type family ‘Case_1627447744’
    In the type family declaration for ‘Case_1627447744’

src/Data/Promotion/Prelude/List.hs:236:3:
    Inaccessible family instance equation:
      Case_1627447744 arg_16274464270 arg_16274464290 '(n0, x0 : xs0)
        = Apply
            (Apply (:$) x0)
            (Apply (Apply TakeSym0 (Apply (Apply (:-$) n0) 1)) xs0)
    In the equations for closed type family ‘Case_1627447744’
    In the type family declaration for ‘Case_1627447744’

Rewriting take to explicitly use case works:

  take                   :: Nat -> [a] -> [a]
  take _ []              =  []
  take n (x:xs)  =  case n <= 0 of
                              True -> []
                              False -> x : take (n-1) xs

Not sure if this is problem with singletons or th-desugar. Needs further investigation.

[goldfirere]

This smells like a desugaring bug. Will examine shortly.

[goldfirere]

This is a desugaring bug, but it's a hard one to fix. The problem is that, when using a pattern guard, there are two possible ways for a match to fail: the pattern matching fails, or the guard eliminates a successful match. Desugaring takes both of these into account.

In the definition of take, the pattern matching can never fail -- it's a universal pattern. But, th-desugar still includes the remaining matches, even though they are now inaccessible.

The solution would be to do a pattern completeness analysis. I believe that this is possible, but it's not a quick fix by any means. As a stop-gap measure, I suppose th-desugar could notice universal patterns and know that these are complete, but that wouldn't solve the problem in all cases.

Regardless, this leads to yet another bug in GHC: overlapped (inaccessible) term-level pattern matches are a warning, but overlapped type-level pattern matches are an error. This is wrong. (It was my design choice, but I take it back.)

I'll implement the "stop-gap" measure and post a bug in th-desugar.

[goldfirere]

This is partially fixed, with the fix to goldfirere/th-desugar#6. Closing as wontfix, as this isn't really singletons's problem.

[jstolarek]

Right. If this isn't singletons problem I'm changing wontifx to invalid ;-)

[goldfirere]

Also, see GHC#9085. When that is fixed, this sort of problem becomes a warning in user code, not an error, which is an improvement.