[GHC] #12677: Type equality in constraint not used?

[GHC]

#12677: Type equality in constraint not used?
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by mpickering:

@@ -2,0 +2,6 @@
+ {-# LANGUAGE TypeInType #-}
+ {-# LANGUAGE GADTs #-}
+ {-# LANGUAGE RankNTypes #-}
+
+ import Data.Kind
+
@@ -7,0 +13,3 @@
+
+ zero :: Type ~ k => TyRep (a :: k) -> a
+ zero = undefine
@@ -9,1 +18,1 @@
- This is allowed:
+ fails with the error
@@ -11,1 +20,9 @@
- {{{#!hs
+ {{{
+ ttest.hs:13:39: error:
+     • Expected a type, but ‘a’ has kind ‘k’
+     • In the type signature: zero :: Type ~ k => TyRep (a :: k) -> a
+ }}}
+
+ But if you replace `zero` with
+
+ {{{
@@ -16,17 +33,1 @@
- but this is not
-
- {{{#!hs
- zero :: Type ~ k => TyRep (a :: k) -> a
- zero = undefined
-
- zero :: TyRep (a :: k) -> Type ~ k => a
- zero = undefined
- }}}
-
- {{{
- tuHu.hs:20:35: error: …
-     • Expected a type, but ‘a’ has kind ‘k’
-     • In the type signature:
-         zero :: Type ~ k => R (a :: k) -> a
- Compilation failed.
- }}}
+ then the program compiles.

New description:

 {{{#!hs
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}

 import Data.Kind

 data TyRep :: forall k. k -> Type where
   TyInt   :: TyRep Int
   TyBool  :: TyRep Bool
   TyMaybe :: TyRep Maybe
   TyApp   :: TyRep f -> TyRep x -> TyRep (f x)

 zero :: Type ~ k => TyRep (a :: k) -> a
 zero = undefine
 }}}

 fails with the error

 {{{
 ttest.hs:13:39: error:
     • Expected a type, but ‘a’ has kind ‘k’
     • In the type signature: zero :: Type ~ k => TyRep (a :: k) -> a
 }}}

 But if you replace `zero` with

 {{{
 zero :: TypeRep (a :: Type) -> a
 zero = undefined
 }}}

 then the program compiles.

--

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