Last active
September 19, 2019 12:34
-
-
Save tdietert/8719b2ffb016925a1ff305384f651233 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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? ------------ | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi, thanks for sending me the gist.
Your error is on line 14. It should read:
The bidirectional system should only binds names for synthesized terms (i.e. Name Syn). However your definition of Pi
was trying to bind a name for a checked term. These are different namespaces.