<NME> DataKinds.hs
<BEF> {-# LANGUAGE DataKinds #-}

module ProxyClass where

import           Data.Proxy

{-@ sizeOfMember :: Proxy a -> Nat @-}
sizeOfMember :: Proxy a -> Int
sizeOfMember = undefined 

<MSG> move into todo-rebare

<DFF> @@ -4,6 +4,11 @@ module ProxyClass where
 
 import           Data.Proxy
 
+-- TODO-REBARE: The following works ...
+{- sizeOfMember :: _ -> Nat @-}
+
+-- TODO-REBARE: ... but this does not. 
 {-@ sizeOfMember :: Proxy a -> Nat @-}
+
 sizeOfMember :: Proxy a -> Int
 sizeOfMember = undefined 
\ No newline at end of file

{'addition_count': 5, 'commit_subject': 'move into todo-rebare', 'deletion_count': 0, 'file_extension': '.hs', 'lang': 'hs', 'license': 'bsd-3-clause', 'repo_name': 'ucsd-progsys/liquidhaskell'}