Re: [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
      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.
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
}}}
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 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

 }}}

--

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