Type literals in Reflection of type constructor kinds leads to SafeHaskell violation
Summary
Data.Typeable.Internal#mkTypeLitFromString has a typo which causes type Natural literals are tagged with the type Symbol type constructor. This can be used to get a TypeRep Nat
that is equal to the true TypeRep Symbol
.
Steps to reproduce
Run this program:
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeOperators, Safe #-}
module Main where
import Data.Maybe
import Data.Proxy
import Type.Reflection
import GHC.TypeLits
data Dat (x :: Proxy 1) = MkD1
evil :: Maybe (Nat :~~: Symbol)
evil = eqTypeRep (case (typeRepKind (typeRep :: TypeRep Dat)) of
(Fun (App _ x) _) -> typeRepKind x)
(typeRep :: TypeRep Symbol)
main :: IO ()
main = print (isJust evil)
The program prints True. This could easily be used to make an unsafeCast.
Expected behavior
The program prints False
Environment
- GHC version used: 8.10.3
Edited by Kyle Ehrlich