Example for GHC bug 10293

README.md

To observe the error:

    $ ghc -c -O Alpha.hs
    $ ghc -c -O -v Calc.hs
    # note Calc.hs hangs on "Called arity analysis"

To make the compilation take longer, add more branches to the Expr datatype.

Alpha.hs

-- |
-- Module     : Unbound.Generics.LocallyNameless.Alpha
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Use the 'Alpha' typeclass to mark types that may contain 'Name's.
{-# LANGUAGE DefaultSignatures
             , FlexibleContexts
             , GADTs
             , DeriveGeneric
             , TypeOperators #-}
module Alpha (
  -- * Name-aware opertions
  Alpha(..)
  -- * Names
  , Name
  , AnyName
  -- * Binding
  , Bind
  -- * Embedding terms in patterns
  , Embed(..)
  -- * Binder variables
  , DisjointSet(..)
  , inconsistentDisjointSet
  , singletonDisjointSet
  , isConsistentDisjointSet
  -- * Implementation details
  , NthPatFind
  , NamePatFind
  , AlphaCtx
  , initialCtx
  , patternCtx
  , termCtx
  , isTermCtx
  , incrLevelCtx
  , decrLevelCtx
  , isZeroLevelCtx
  -- * Internal
  , gaeq
  , gisPat
  , gisTerm
  , gnthPatFind
  , gnamePatFind
  , gswaps
  , gfreshen
  ) where

import Control.Applicative (Applicative(..), (<$>))
import Control.Arrow (first)
import Control.Monad (liftM)
import Data.Function (on)
import Data.Foldable (Foldable(..))
import Data.List (intersect)
import Data.Monoid (Monoid(..), (<>))
import Data.Ratio (Ratio)
import Data.Typeable (Typeable, gcast, typeOf)
import GHC.Generics

-- | The @Fresh@ type class governs monads which can generate new
--   globally unique 'Name's based on a given 'Name'.
class Monad m => Fresh m where

  -- | Generate a new globally unique name based on the given one.
  fresh :: Name a -> m (Name a)

-- | Types that are instances of @Alpha@ may participate in name representation.
--
-- Minimal instance is entirely empty, provided that your type is an instance of
-- 'Generic'.
class (Show a) => Alpha a where
  -- | See 'Unbound.Generics.LocallyNameless.Operations.aeq'.
  aeq' :: AlphaCtx -> a -> a -> Bool
  default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool
  aeq' c = (gaeq c) `on` from

  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid pattern.
  isPat :: a -> DisjointSet AnyName
  default isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName
  isPat = gisPat . from

  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid term.
  isTerm :: a -> Bool
  default isTerm :: (Generic a, GAlpha (Rep a)) => a -> Bool
  isTerm = gisTerm . from

  -- | @isEmbed@ is needed internally for the implementation of
  --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero
  --   or more occurrences of 'Shift'.  The default implementation
  --   simply returns @False@.
  isEmbed :: a -> Bool
  isEmbed _ = False

  -- | If @a@ is a pattern, finds the @n@th name in the pattern
  -- (starting from zero), returning the number of names encountered
  -- if not found.
  nthPatFind :: a -> NthPatFind
  default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind
  nthPatFind = gnthPatFind . from

  -- | If @a@ is a pattern, find the index of the given name in the pattern.
  namePatFind :: a -> NamePatFind
  default namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind
  namePatFind = gnamePatFind . from

  -- | See 'Unbound.Generics.LocallyNameless.Operations.swaps'. Apply
  -- the given permutation of variable names to the given pattern.
  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
  default swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a
  swaps' ctx perm = to . gswaps ctx perm . from

  -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.  Rename the free variables
  -- in the given term to be distinct from all other names seen in the monad @m@.
  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
  default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
  freshen' ctx = liftM (first to) . gfreshen ctx . from

-- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the
-- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@
-- is the @i@th name in @a@
type NthPatFind = Integer -> Either Integer AnyName

-- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that
-- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name
-- in @a@
type NamePatFind = AnyName -> Either Integer Integer -- Left - names skipped over
                                                     -- Right - index of the name we found

-- | The "Generic" representation version of 'Alpha'
class GAlpha f where
  gaeq :: AlphaCtx -> f a -> f a -> Bool

  gisPat :: f a -> DisjointSet AnyName
  gisTerm :: f a -> Bool

  gnthPatFind :: f a -> NthPatFind
  gnamePatFind :: f a -> NamePatFind

  gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a
  gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName)

instance (Alpha c) => GAlpha (K1 i c) where
  gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2

  gisPat = isPat . unK1
  gisTerm = isTerm . unK1

  gnthPatFind = nthPatFind . unK1
  gnamePatFind = namePatFind . unK1

  gswaps ctx perm = K1 . swaps' ctx perm . unK1
  gfreshen ctx = liftM (first K1) . freshen' ctx . unK1

instance GAlpha f => GAlpha (M1 i c f) where
  gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2

  gisPat = gisPat . unM1
  gisTerm = gisTerm . unM1

  gnthPatFind = gnthPatFind . unM1
  gnamePatFind = gnamePatFind . unM1

  gswaps ctx perm = M1 . gswaps ctx perm . unM1
  gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1

instance GAlpha U1 where
  gaeq _ctx _ _ = True

  gisPat _ = mempty
  gisTerm _ = True

  gnthPatFind _ = Left
  gnamePatFind _ _ = Left 0

  gswaps _ctx _perm _ = U1
  gfreshen _ctx _ = return (U1, mempty)

instance GAlpha V1 where
  gaeq _ctx _ _ = False

  gisPat _ = mempty
  gisTerm _ = False

  gnthPatFind _ = Left
  gnamePatFind _ _ = Left 0

  gswaps _ctx _perm _ = undefined
  gfreshen _ctx _ = return (undefined, mempty)

instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where
  gaeq ctx (f1 :*: g1) (f2 :*: g2) =
    gaeq ctx f1 f2 && gaeq ctx g1 g2

  gisPat (f :*: g) = gisPat f <> gisPat g
  gisTerm (f :*: g) = gisTerm f && gisTerm g

  gnthPatFind (f :*: g) i = case gnthPatFind f i of
    Left i' -> gnthPatFind g i'
    Right ans -> Right ans
  gnamePatFind (f :*: g) n = case gnamePatFind f n of
    Left j -> case gnamePatFind g n of
      Left i -> Left $! j + i
      Right k -> Right $! j + k
    Right k -> Right k

  gswaps ctx perm (f :*: g) =
    gswaps ctx perm f :*: gswaps ctx perm g

  gfreshen ctx (f :*: g) = do
    (g', perm2) <- gfreshen ctx g
    (f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)
    return (f' :*: g', perm1 <> perm2)

instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where
  gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2
  gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2
  gaeq _ctx _       _       = False

  gisPat (L1 f) = gisPat f
  gisPat (R1 g) = gisPat g

  gisTerm (L1 f) = gisTerm f
  gisTerm (R1 g) = gisTerm g

  gnthPatFind (L1 f) i = gnthPatFind f i
  gnthPatFind (R1 g) i = gnthPatFind g i
  
  gnamePatFind (L1 f) n = gnamePatFind f n
  gnamePatFind (R1 g) n = gnamePatFind g n

  gswaps ctx perm (L1 f) = L1 (gswaps ctx perm f)
  gswaps ctx perm (R1 f) = R1 (gswaps ctx perm f)

  gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)
  gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)
  
-- ============================================================
-- Alpha instances for the usual types

instance Alpha Int where
  aeq' _ctx i j = i == j

  isPat _ = mempty
  isTerm _ = True

  nthPatFind _ = Left
  namePatFind _ _ = Left 0

  swaps' _ctx _p i = i
  freshen' _ctx i = return (i, mempty)

instance Alpha Char where
  aeq' _ctx i j = i == j

  isPat _ = mempty
  isTerm _ = True

  nthPatFind _ = Left
  namePatFind _ _ = Left 0

  swaps' _ctx _p i = i
  freshen' _ctx i = return (i, mempty)

instance Alpha Integer where
  aeq' _ctx i j = i == j

  isPat _ = mempty
  isTerm _ = True

  nthPatFind _ = Left
  namePatFind _ _ = Left 0

  swaps' _ctx _p i = i
  freshen' _ctx i = return (i, mempty)

instance Alpha Bool

instance Alpha a => Alpha (Maybe a)
instance Alpha a => Alpha [a]
instance Alpha ()
instance (Alpha a,Alpha b) => Alpha (Either a b)
instance (Alpha a,Alpha b) => Alpha (a,b)
instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
   Alpha (a,b,c,d,e)

-- ============================================================
-- Alpha instances for interesting types

instance Typeable a => Alpha (Name a) where
  aeq' ctx n1 n2 =
    if isTermCtx ctx
    then n1 == n2 -- in terms, better be the same name
    else True     -- in a pattern, names are always equivlent (since
                  -- they're both bound, so they can vary).

  isPat n = if isFreeName n
            then singletonDisjointSet (AnyName n)
            else inconsistentDisjointSet

  isTerm _ = True

  nthPatFind nm i =
    if i == 0 then Right (AnyName nm) else Left $! i-1

  namePatFind nm1 (AnyName nm2) =
    case gcast nm1 of
      Just nm1' -> if nm1' == nm2 then Right 0 else Left 1
      Nothing -> Left 1

  swaps' ctx perm nm =
    if isTermCtx ctx
    then case applyPerm perm (AnyName nm) of
      AnyName nm' ->
        case gcast nm' of
          Just nm'' -> nm''
          Nothing -> error "Internal error swaps' on a Name returned permuted name of wrong sort"
    else nm
      
  freshen' ctx nm =
    if not (isTermCtx ctx)
    then do
      nm' <- fresh nm
      return (nm', single (AnyName nm) (AnyName nm'))
    else error "freshen' on a Name in term position"

instance Alpha AnyName where
  aeq' ctx x y =
    if x == y
    then True
    else
      -- in a term unequal variables are unequal, in a pattern it's
      -- ok.
      not (isTermCtx ctx)

  isTerm _ = True

  isPat n@(AnyName nm) = if isFreeName nm
                         then singletonDisjointSet n
                         else inconsistentDisjointSet

  swaps' ctx perm n =
    if isTermCtx ctx
    then applyPerm perm n
    else n

  freshen' ctx (AnyName nm) =
    if isTermCtx ctx
    then error "LocallyNameless.freshen' on AnyName in Term mode"
    else do
      nm' <- fresh nm
      return (AnyName nm', single (AnyName nm) (AnyName nm'))

  nthPatFind nm i =
    if i == 0 then Right nm else Left $! i - 1

  namePatFind nmHave nmWant =
    if nmHave == nmWant
    then Right 0
    else Left 1

data Name a = Fn String !Integer    -- free names
            | Bn !Integer !Integer  -- bound names / binding level + pattern index
            deriving (Eq, Ord, Typeable, Generic)

-- | Returns 'True' iff the given @Name a@ is free.
isFreeName :: Name a -> Bool
isFreeName (Fn _ _) = True
isFreeName _ = False

-- | Make a free 'Name a' from a 'String'
string2Name :: String -> Name a
string2Name s = makeName s 0

-- | Synonym for 'string2Name'.
s2n :: String -> Name a
s2n = string2Name

-- | Make a name from a 'String' and an 'Integer' index
makeName :: String -> Integer -> Name a
makeName = Fn

-- | Get the integer part of a 'Name'.
name2Integer :: Name a -> Integer
name2Integer (Fn _ i) = i
name2Integer (Bn _ _) = error "Internal Error: cannot call name2Integer for bound names"

-- | Get the string part of a 'Name'.
name2String :: Name a -> String
name2String (Fn s _) = s
name2String (Bn _ _) = error "Internal Error: cannot call name2String for bound names"

instance Show (Name a) where
  show (Fn "" n) = "_" ++ (show n)
  show (Fn x 0) = x
  show (Fn x n) = x ++ (show n)
  show (Bn x y) = show x ++ "@" ++ show y

-- | An @AnyName@ is a name that stands for a term of some (existentially hidden) type.
data AnyName where
  AnyName :: Typeable a => Name a -> AnyName

instance Show AnyName where
  show (AnyName nm) = show nm

instance Eq AnyName where
  (AnyName n1) == (AnyName n2) = case gcast n2 of
    Just n2' -> n1 == n2'
    Nothing -> False


-- | A term of type @'Bind' p t@ is a term that binds the free
-- variable occurrences of the variables in pattern @p@ in the term
-- @t@.  In the overall term, those variables are now bound. See also
-- 'Unbound.Generics.LocallyNameless.Operations.bind' and
-- 'Unbound.Generics.LocallyNameless.Operations.unbind' and
-- 'Unbound.Generics.LocallyNameless.Operations.lunbind'
data Bind p t = B p t
              deriving (Generic)

instance (Show p, Show t) => Show (Bind p t) where
  showsPrec prec (B p t) =
    showParen (prec > 0) (showString "<"
                          . showsPrec prec p
                          . showString "> "
                          . showsPrec 0 t)

instance (Alpha p, Alpha t) => Alpha (Bind p t) where

  aeq' ctx (B p1 t1) (B p2 t2) =
    aeq' (patternCtx ctx) p1 p2
    && aeq' (incrLevelCtx ctx) t1 t2

  isPat _ = inconsistentDisjointSet

  isTerm (B p t) = isConsistentDisjointSet (isPat p) && isTerm t

  nthPatFind b = error $ "Binding " ++ show b ++ " used as a pattern"
  namePatFind b = error $ "Binding " ++ show b ++ " used as a pattern"

  swaps' ctx perm (B p t) =
    B (swaps' (patternCtx ctx) perm p)
      (swaps' (incrLevelCtx ctx) perm t)

-- | @Embed@ allows for terms to be /embedded/ within patterns.  Such
--   embedded terms do not bind names along with the rest of the
--   pattern.  For examples, see the tutorial or examples directories.
--
--   If @t@ is a /term type/, then @Embed t@ is a /pattern type/.
--
--   @Embed@ is not abstract since it involves no binding, and hence
--   it is safe to manipulate directly.  To create and destruct
--   @Embed@ terms, you may use the @Embed@ constructor directly.
--   (You may also use the functions 'embed' and 'unembed', which
--   additionally can construct or destruct any number of enclosing
--   'Shift's at the same time.)
newtype Embed t = Embed t deriving (Eq, Generic)

instance Show a => Show (Embed a) where
  showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}"

instance Alpha t => Alpha (Embed t) where
  isPat (Embed t) = if (isTerm t) then mempty else inconsistentDisjointSet

  isTerm _ = False

  isEmbed (Embed t) = isTerm t

  swaps' ctx perm (Embed t) =
    if isTermCtx ctx
    then Embed t
    else Embed (swaps' (termCtx ctx) perm t)

  aeq' ctx (Embed x) (Embed y) = aeq' (termCtx ctx) x y

  nthPatFind _ = Left
  namePatFind _ _ = Left 0

-- | Some 'Alpha' operations need to record information about their
-- progress.  Instances should just pass it through unchanged.
--
-- The context records whether we are currently operating on terms or patterns,
-- and how many binding levels we've descended.
data AlphaCtx = AlphaCtx { ctxMode :: !Mode, ctxLevel :: !Integer }

newtype Perm a = Perm { applyPerm :: a -> a }

instance Eq a => Monoid (Perm a) where
  mempty = Perm id
  mappend p1 p2 = undefined

single :: a -> a -> Perm a
single x y = undefined


data Mode = Term | Pat
          deriving Eq

-- | The starting context for alpha operations: we are expecting to
-- work on terms and we are under no binders.
initialCtx :: AlphaCtx
initialCtx = AlphaCtx { ctxMode = Term, ctxLevel = 0 }

-- | Switches to a context where we expect to operate on patterns.
patternCtx :: AlphaCtx -> AlphaCtx
patternCtx ctx = ctx { ctxMode = Pat }

-- | Switches to a context where we expect to operate on terms.
termCtx :: AlphaCtx -> AlphaCtx
termCtx ctx = ctx { ctxMode = Term }

-- | Returns 'True' iff we are in a context where we expect to see terms.
isTermCtx :: AlphaCtx -> Bool
isTermCtx (AlphaCtx {ctxMode = Term}) = True
isTermCtx _                           = False

-- | Increment the number of binders that we are operating under.
incrLevelCtx :: AlphaCtx -> AlphaCtx
incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx }

-- | Decrement the number of binders that we are operating under.
decrLevelCtx :: AlphaCtx -> AlphaCtx
decrLevelCtx ctx = ctx { ctxLevel = ctxLevel ctx - 1 }

-- | Are we operating under no binders?
isZeroLevelCtx :: AlphaCtx -> Bool
isZeroLevelCtx ctx = ctxLevel ctx == 0

-- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal
-- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'.
--
-- @
--   inconsistentDisjointSet \<> s == inconsistentDisjointSet
--   s \<> inconsistentDisjoinSet == inconsistentDisjointSet
-- @
newtype DisjointSet a = DisjointSet (Maybe [a])

instance Eq a => Monoid (DisjointSet a) where
  mempty = DisjointSet (Just [])
  mappend s1 s2 =
    case (s1, s2) of
      (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))
      _ -> inconsistentDisjointSet

instance Foldable DisjointSet where
  foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms

-- | Returns a @DisjointSet a@ that is the annihilator element for the 'Monoid' instance of 'DisjointSet'.
inconsistentDisjointSet :: DisjointSet a
inconsistentDisjointSet = DisjointSet Nothing

-- | @singletonDisjointSet x@ a @DisjointSet a@ that contains the single element @x@
singletonDisjointSet :: a -> DisjointSet a
singletonDisjointSet x = DisjointSet (Just [x])

disjointLists :: Eq a => [a] -> [a] -> Bool
disjointLists xs ys = null (intersect xs ys)

-- | @isConsistentDisjointSet@ returns @True@ iff the given disjoint set is not inconsistent.
isConsistentDisjointSet :: DisjointSet a -> Bool
isConsistentDisjointSet (DisjointSet Nothing) = False
isConsistentDisjointSet _ = True

Calc.hs

-- |
-- Module     : Calc
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
module Calc where

import Control.Arrow (second)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)

import Alpha

-- variables will range over expressions
type Var = Name Expr

-- expression is either a variable, a constant int, a summation of two
-- expressions, a list of variables bound to expressions that may
-- occur in the body of an expression (where the expressions in the
-- list of bindings refer to an outer scope), or a sequence of nested bindings
-- where each binding expression can refer to previously bound variables.
data Expr = V Var
          | C Int
          | Add Expr Expr
          | Lam (Bind Var Expr)
          | App Expr Expr
          | Let (Bind [(Var, Embed Expr)] Expr)
          | Case Expr [Match]
          deriving (Generic, Typeable, Show)

data Match = Match (Bind Var Expr)
           deriving (Generic, Typeable, Show)

instance Alpha Expr
instance Alpha Match