Skip to content

GitLab

Closed
Opened by Kyle Ehrlich@KyleDavidE

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