[GHC] #12677: Type equality in constraint not used?
#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- {{{#!hs data TyRep :: forall k. k -> Type where TyInt :: TyRep Int TyBool :: TyRep Bool TyMaybe :: TyRep Maybe TyApp :: TyRep f -> TyRep x -> TyRep (f x) }}} This is allowed: {{{#!hs zero :: TypeRep (a :: Type) -> a zero = undefined }}} 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. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): This is a hard one to fix, surprisingly. The problem is that you've declared `a` to have type `k` and then used `a` as an argument to `->`. Of course, `->` expects a `Type`. So GHC should insert add a cast, forming `a |> η`, for the argument to `->`. The problem is that this would require using the equality proof for `Type ~ k` as the body of `η`, and the current type system simply does not allow this. [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unl... Here] are some notes on the matter, though they were not written to be digested by anyone but me. I don't expect this will be fixed until we have `-XDependentTypes`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: #13337 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) * related: => #13337 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: #13337, #15710 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #13337 => #13337, #15710 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: #13337, #15710 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
The problem is that this would require using the equality proof for Type ~ k as the body of η
Doesn't coercion quantification help with this? (Though as so often, I'm worried about the difference between `(Type ~ k)` and `(Type ~# k)`.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: #13337, #15710 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think this is #15710. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC