{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuasiQuotes #-}
module Main where

import Language.Haskell.TH
import Control.Proof.TH

data X = X
data Y = Y deriving Show
f :: X -> Y
f X = Y
x :: X
x = X

[d| |] -- required to the reify.

y :: Y
y = $(prove ['f,'x] [t| Y |])

y' :: Y
y' = $(prove ['f,'X] [t| Y |])

y'' :: Y
y'' = $(prove ['f,''X] [t| Y |])

main :: IO ()
main = print y'
