More Typed Template Haskell unsoundness due to levity polymorphism
The levity polymorphism check does not run on quoted expressions which means you can use quotes to define a levity polymorphic code generator.
This leads to unsoundness as a well-typed code generator leads to an ill-typed program.
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module Bad where
import Language.Haskell.TH.Lib
import GHC.Exts
-- Example from the user guide but with the function wrapped in quotes
bad :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
TExpQ ((a -> b) -> a -> b)
bad = [|| \f x -> f x ||]
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module Lev where
import Language.Haskell.TH.Lib
import Bad
import GHC.Exts
-- Code generator type checked but splicing fails to produce well-typed
-- program -- unsound
unsound :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
((a -> b) -> a -> b)
unsound = $$(bad)
-- Generating a monomorphic program is sound, and hence a workaround for
-- normal levity polymorphic restrictions.
workaround :: Int
workaround = $$bad id 5
https://gist.github.com/144e42b4429673d8449f59413cc10ca4
cc @RyanGlScott who was interested in this issue.