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.