[GHC] #15558: Locally handling an empty constraint

22 Aug 2018

      #15558: Locally handling an empty constraint
-------------------------------------+-------------------------------------
           Reporter:  Ericson2314    |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:  ⊥
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  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:
-------------------------------------+-------------------------------------
 I need something like `\case {}` for constraints. See the code below.
 There's nothing I can replace the `undefined` with that will satisfy the
 type checker. The dead code warning also bubbled up out of the field
 incorrectly.

 I think this will require new language features tangentially related to
 Lambdas for `forall`. (Both `forall _.` and `=>` are invisible
 quantifiers.) I will link this ticket in that GHC proposal, but am making
 it's own issue in the first place in case this is a genuine bug that can
 be fixed by less intrusive means.

 {{{
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 module Asdf where

 import Data.Kind
 import Data.Type.Equality

 data Sing a where
   X :: Sing Int
   Y :: Sing [Bool]

 data Foo a = Foo a (forall b. [b] :~: a -> b)
 data Bar a = Bar a (forall b. [b] ~ a => b)

 f, f' :: forall a. Sing a -> Foo a

 f s = Foo a b
   where
     a :: a
     a = case s of
       X -> 0
       Y -> []
     b :: forall b. [b] :~: a -> b
     b = case s of
       X -> \case {}
       Y -> \Refl -> False

 f' = \case
   X -> Foo 0  (\case {})
   Y -> Foo [] (\Refl -> False)

 g, g' :: forall a. Sing a -> Bar a

 g s = Bar a b
   where
     a :: a
     a = case s of
       X -> 0
       Y -> []
     b :: forall b. [b] ~ a => b
     b = case s of
       Y -> False

 g' = \case
   X -> Bar 0 undefined -- can't make this happy
   Y -> Bar [] False

 }}}

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