T1555.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--rankNTypes" @-}
{-# LANGUAGE RankNTypes   #-}

module Theorems where

import Language.Haskell.Liquid.Equational 

type ForAll a  = forall z. a
data Wrapper a = Wrapper (ForAll a)
 
foo :: ForAll a -> ForAll a  -> Proof
{-@ foo :: ff:ForAll a -> gg:{ForAll a | ff == gg } -> { Wrapper ff == Wrapper gg } @-} 
foo g f = Wrapper g ==. Wrapper f *** QED