[GHC] #15558: Locally handling an empty constraint

[GHC]

#15558: Locally handling an empty constraint
-------------------------------------+-------------------------------------
        Reporter:  Ericson2314       |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:  ⊥
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------
Description changed by Ericson2314:

Old description:

> I need something like `\case {}` for constraints. See the code below. The
> undefined won't satisfy the type checker, nor is there anything total I
> found that I could replace it with that would. 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
>
> }}}

New description:

 I need something like `\case {}` for constraints. See the code below. The
 `undefined` won't satisfy the type checker, nor is there anything total I
 found that would. 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#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler