Bad.hs

{-# 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 ||]

Lev.hs

{-# 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