[GHC] #13337: GHC doesn't think a type is of kind *, despite having evidence for it
GHC
ghc-devs at haskell.org
Sun Feb 26 16:21:39 UTC 2017
#13337: GHC doesn't think a type is of kind *, despite having evidence for it
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.2
checker) |
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
Another way to phrase my question is: I don't see what the distinction
between the first and second examples is. After all, you can rewrite the
second example like this:
{{{#!hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing -> "Non-Type kind"
Just Refl -> go_on eqT
where
go_on :: Maybe (a :~: Int) -> String
go_on Nothing = "Non-Int type"
go_on (Just Refl) = "It's an Int!"
}}}
Now the equality assumption isn't coming into scope "only in an expression
of that type", it's coming into scope in a type signature! So again,
unless I'm misunderstanding something, I strongly suspect that fixing the
second program would naturally lend itself towards fixing the first
program.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13337#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list