Using equality constraint in datatype kind signature leads to various strange behaviors
The following file
{-# LANGUAGE DataKinds , TypeFamilies #-}
module Weird where
import Data.Kind
type Weird :: forall a -> (a ~ Char) => Type
data Weird a = MkWeird a
deriving Show
allows this GHCi session:
ghci> :t MkWeird
-- This looks like a kind error, and is impossible to write
MkWeird :: forall a {ev :: a ~ Char}. a -> Weird a
ghci> MkWeird "foo"
-- this is fine - but shouldn't be! The argument to MkWeird must be a Char, not String
MkWeird "foo"
ghci> :t MkWeird "foo"
-- We can ask for the type
MkWeird "foo" :: Weird String
ghci> :t MkWeird "foo" :: Weird String
-- but checking that same type results in a kind error
-- (shouldn't this be a type error instead?)
<interactive>:1:18: error:
* Couldn't match kind `[Char]' with `Char'
[...]
ghci> import Data.Dynamic
ghci> Data.Dynamic.toDyn (MkWeird 'c' :: Weird Char)
-- what is <>?
<interactive>:50:1: error:
* No instance for (Typeable <>) arising from a use of `toDyn'
[...]
ghci> :i Show
-- The derived Show instance would be impossible to write manually
[...]
instance forall a (ev :: a ~ Char). Show a => Show (Weird a)
[...]
Environment
- GHC version used: 9.3.20210529
Optional:
- Operating System: Arch on WSL2 on Windows 10
- System Architecture: x86_64