[GHC] #16278: Exhaustivity checking GADT with free variables

2 Feb 2019

      #16278: Exhaustivity checking GADT with free variables
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following example:

 {{{#!hs
 {-# language DataKinds #-}
 {-# language TypeFamilies #-}
 {-# language GADTs #-}
 {-# language KindSignatures #-}

 {-# OPTIONS_GHC -Wall -fforce-recomp #-}

 module GadtException where

 import Data.Kind (Type)
 import GHC.Exts

 data Send = Send

 data SocketException :: Send -> Type where
   LocalShutdown :: SocketException 'Send
   OutOfMemory :: SocketException a

 someSocketException :: SocketException a
 someSocketException = OutOfMemory

 foo :: Int
 foo = case someSocketException :: SocketException Any of
   LocalShutdown -> 2
   OutOfMemory -> 1
 }}}

 In `foo`, GHC's exhaustivity checker requires a pattern match on
 `LocalShutdown`. However, `LocalShutdown` is not an inhabitant of
 `SocketException Any`. What I would really like is for this to go one step
 further. I shouldn't even need to write the type annotation. That is, with
 the above code otherwise unchanged, GHC should recognize that

 {{{#!hs
 foo :: Int
 foo = case someSocketException of
   OutOfMemory -> 1
 }}}

 handles all possible cases. Since fully polymorphic type variables become
 `Any` at some point during typechecking, I would expect that if this
 worked with the `SocketException Any` type signature, it would work
 without it.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler