-- FAILING TEST: this test SHOULD FAIL BUT DOESN'T
-- issue #519
{-# LANGUAGE DeriveFunctor #-}
module AST where
data AstIndex = IxExpr | IxType
{-@ measure isExprIndex @-}
isExprIndex :: AstIndex -> Bool
isExprIndex IxExpr = True
isExprIndex _ = False
{-@ measure isTypeIndex @-}
isTypeIndex :: AstIndex -> Bool
isTypeIndex IxType = True
isTypeIndex _ = False
data AstF f = Lit Int AstIndex
| Var String AstIndex
| App f f
| Paren f
{-@
data AstF f <ix :: AstIndex -> Bool>
= Lit {lv :: Int , i :: AstIndex<ix>}
| Var {vv :: String, i :: AstIndex<ix>}
| App (fn :: f) (arg :: f)
| Paren (ast :: f)
@-}
{-@ type AstFE = AstF <{\ix -> isExprIndex ix}> @-}
{-@ type AstFT = AstF <{\ix -> isTypeIndex ix}> @-}
-- Now lets tie the knot!
newtype Fix f = In { out :: f (Fix f) }
type Ast = Fix AstF
{-@ type AstE = Fix AstFE @-}
{-@ type AstT = Fix AstFT @-}
{-@ astExpr :: Fix (AstF <{\ix -> isExprIndex ix}>) @-}
astExpr :: Ast
astExpr = undefined
{-@ id1 :: forall <p :: AstIndex -> Bool>. Fix (AstF <p>) -> Fix (AstF <p>) @-}
id1 :: Fix AstF -> Fix AstF
id1 z = z
{-@ wrong :: AstT @-}
wrong = id1 astExpr