[GHC] #14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is

[GHC]

#14813: EmptyCase thinks pattern match involving type family is not exhaustive,
when it actually is
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Actually, I think the issue may be in an entirely different place than
 what I originally suspected, and the fact that it surfaces in `EmptyCase`
 may be entirely coincidental. Consider the following program, which uses
 an ordinary pattern-match:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wall #-}
 module Bug where

 data Unit = MkUnit

 data SUnit (u :: Unit) where
   SMkUnit :: SUnit 'MkUnit

 type family F (u :: Unit) where
   F 'MkUnit = ()

 absoluteUnit :: SUnit u -> F u -> ()
 absoluteUnit SMkUnit x = case x of { () -> () }
 }}}

 Things get interesting when you try to put wildcard types on various
 spots. For example, if you put one on the scrutinee of the `case`
 expression:

 {{{#!hs
 absoluteUnit :: SUnit u -> F u -> ()
 absoluteUnit SMkUnit x = case (x :: _) of { () -> () }
 }}}

 Then this is what GHC gives back:

 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:17:37: error:
     • Found type wildcard ‘_’ standing for ‘F 'MkUnit’
       To use the inferred type, enable PartialTypeSignatures
     • In an expression type signature: _
       In the expression: (x :: _)
       In the expression: case (x :: _) of { () -> () }
     • Relevant bindings include
         x :: F u (bound at Bug.hs:17:22)
         absoluteUnit :: SUnit u -> F u -> () (bound at Bug.hs:17:1)
    |
 17 | absoluteUnit SMkUnit x = case (x :: _) of { () -> () }
    |                                     ^
 }}}

 Note that it says `x`'s type is `F 'MkUnit`, not `()`! To make things
 stranger, if you put an additional wildcard type on the binder for `x`:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wall #-}
 module Bug where

 data Unit = MkUnit

 data SUnit (u :: Unit) where
   SMkUnit :: SUnit 'MkUnit

 type family F (u :: Unit) where
   F 'MkUnit = ()

 absoluteUnit :: SUnit u -> F u -> ()
 absoluteUnit SMkUnit (x :: _) = case (x :: _) of { () -> () }
 }}}

 Now GHC claims the type of both wildcards is `()`!

 All this makes me believe that somehow, the typechecker isn't giving the
 correct type (or at least, an insufficiently type-family-free–type) to `x`
 unless you explicitly prod GHC with redundant typing information.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler