Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

unbind2Plus doesn't work with two different pattern types #50

Open
liesnikov opened this issue Oct 31, 2022 · 1 comment
Open

unbind2Plus doesn't work with two different pattern types #50

liesnikov opened this issue Oct 31, 2022 · 1 comment
Labels

Comments

@liesnikov
Copy link
Contributor

liesnikov commented Oct 31, 2022

using unbind2Plus on two different term types results in an error when printing the terms out, see an example below.

Using it on two terms of the same type doesn't cause errors, as far as I can see.

Example

{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}

import qualified Unbound.Generics.LocallyNameless as Unbound
import           GHC.Generics (Generic)
import           Control.DeepSeq (NFData, force)

type LName = Unbound.Name LTerm

data LTerm
  = -- | variables  `x`
    LVar LName
  | -- | abstraction  `\x. a`
    LLam (Unbound.Bind LName LTerm)
  | -- | application `a b`
    LApp LTerm LTerm
  deriving (Show, Generic, Unbound.Alpha, NFData)

type RName = Unbound.Name RTerm

data RTerm
  = -- | variables  `x`
    RVar RName
  | -- | abstraction  `\x. a`
    RLam (Unbound.Bind RName RTerm)
  | -- | application `a b`
    RApp RTerm RTerm
  deriving (Show, Generic, Unbound.Alpha, NFData)

lterm :: LTerm
lterm =
  let name = (Unbound.s2n "left")
      var = LVar name
  in LLam (Unbound.bind name var)

rterm :: RTerm
rterm =
  let name = (Unbound.s2n "right")
      var = RVar name
  in RLam (Unbound.bind name var)

test :: IO (LTerm, RTerm)
test = Unbound.runFreshMT $ do
  let (LLam lbind) = lterm
  let (RLam rbind) = rterm
  (lv, lb, rv, rb) <- Unbound.unbind2Plus lbind rbind
  return (lb, rb)

main :: IO ()
main = do
  (l,r) <- test
-- this doesn't cause errors
  let dl = force l
  let dr = force r
-- this does
  putStrLn $ show $ dl
  putStrLn $ show $ dr
-- that's it
  putStrLn "done"

Error

The error I'm getting while printing the right subterm is

LocallyNameless.open: inconsistent sorts
CallStack (from HasCallStack):
error, called at src/Unbound/Generics/LocallyNameless/Alpha.hs:717:20 in unbound-generics-0.4.2-B2j2SNQtM51IWCI7gQ83CW:Unbound.Generics.LocallyNameless.Alpha

Version

this is using GHC 9.02, but also works on at least 9.2.2
unbound-generics version is the current revision a2a5580

How to build the example

I have this example in a reproducible build. Here is a gist with all relevant files.

@liesnikov
Copy link
Contributor Author

The workaround I settled for is using unbind separately on the two terms, i.e.

let (lv, lb) <- Unbound.unbind lterm
    (rv, rb) <- Unbound.unbind rterm
in ...

instead of (lv, lb, rv, rb) <- Unbound.unbind2Plus lbind rbind.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants