UnboundIssue.hs

{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE MultiParamTypeClasses      #-}

module Issue where

import  Data.Typeable (Typeable)
import  GHC.Generics (Generic)
import  Unbound.Generics.LocallyNameless

-- | Variables in type-inferable terms
type Var = Name Syn

-- | Telescope with a single element
type UniTele expr = Rebind (Name expr, Embed expr) ()

mkUniTele :: (Alpha expr, Typeable expr) => [Char] -> expr -> UniTele expr
mkUniTele x e = rebind (s2n x, Embed e) ()

-- | Type-inferable (synthesizable) terms
data Syn
  = Var Var -- ^ Free and bound variables
  | Ann Chk Chk -- ^ Annoted terms
  | App Syn Chk -- ^ Application
  | Pi (Bind (UniTele Chk) Chk)-- ^ The term for arrow types
  | Star -- ^ The term for kinds of types
  deriving (Show, Generic)

instance Alpha Syn

instance Subst Syn Syn where
  isvar (Var x) = Just (SubstName x)
  isvar _       = Nothing

-- | Type-checkable Terms
data Chk
  = Inf Syn -- ^ Inferable terms embedded in checkable terms
  | Lam (Bind Var Chk) -- ^ Lambda term
  deriving (Show, Generic)

instance Alpha Chk

instance Subst Chk Syn
instance Subst Chk Chk
instance Subst Syn Chk where
  isCoerceVar (Inf (Var x)) = Just (SubstCoerce x (Just . Inf))
  isCoerceVar _ = Nothing

{- GHCi session initiated with stack:

thomasd@gibbon:~/github/lambda-pi (master)*$ stack ghci src/Issue.hs 
Using configuration for lambda-pi:lib to load /home/thomasd/github/lambda-pi/src/Issue.hs
lambda-pi> initial-build-steps (lib + exe)
Configuring GHCi with the following packages: lambda-pi
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
*** WARNING: /home/thomasd/.ghci is writable by someone else, IGNORING!
Suggested fix: execute 'chmod go-w /home/thomasd/.ghci'
[1 of 1] Compiling Issue            ( /home/thomasd/github/lambda-pi/src/Issue.hs, interpreted )
Ok, one module loaded.
Loaded GHCi configuration from /run/user/1000/haskell-stack-ghci/bb565fe7/ghci-script
*Issue> Pi (bind (mkUniTele "a" (Inf Star)) (Inf (Pi (bind (mkUniTele "_" (Inf (Var (s2n "a")))) (Inf (Var (s2n "a")))))))
Pi (<(<<(a,{Inf Star})>> ())> Inf (Pi (<(<<(_,{Inf (Var a)})>> ())> Inf (Var a))))
                                                    ^^^^^                ^^^^^
                                                      |____________________|
                                                                 |
      Why are these variables not captured?           ------------

-}

--------------------------------------------------------------------------------

type SVar = Name SSyn

data SSyn
  = SVar SVar -- ^ Free and bound variables
  | SAnn SSyn SSyn
  | SApp SSyn SSyn -- ^ Application
  | SPi (Bind (UniTele SSyn) SSyn)-- ^ The term for arrow types
  | SStar -- ^ The term for kinds of types
  | SLam (Bind SVar SSyn) -- ^ The term for kinds of types
  deriving (Show, Generic)

instance Alpha SSyn
instance Subst SSyn SSyn where
  isvar (SVar x) = Just (SubstName x)
  isvar _       = Nothing

{- GHCi session continued:

*Issue> SPi (bind (mkUniTele "a" SStar) (SPi (bind (mkUniTele "_" (SVar (s2n "a"))) (SVar (s2n "a")))))
SPi (<(<<(a,{SStar})>> ())> SPi (<(<<(_,{SVar 0@0})>> ())> SVar 1@0))
                                              ^^^               ^^^
                                               |_________________|
                                                        |
            But these variables are?         ------------

-}

Hi, thanks for sending me the gist.

Your error is on line 14. It should read:

type UniTele expr = Rebind (Name Syn, Embed expr) ()

The bidirectional system should only binds names for synthesized terms (i.e. Name Syn). However your definition of Pi

 | Pi (Bind (UniTele Chk) Chk)

was trying to bind a name for a checked term. These are different namespaces.