Skip to content

Instantly share code, notes, and snippets.

@liesnikov
Last active October 31, 2022 14:07
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save liesnikov/67b8aaa45357e927254bf44ae2f234a0 to your computer and use it in GitHub Desktop.
Save liesnikov/67b8aaa45357e927254bf44ae2f234a0 to your computer and use it in GitHub Desktop.
Reproducing a bug in unbound-generics https://github.com/lambdageek/unbound-generics/issues/50

Steps to reproduce:

  1. Download files into a new directory
  2. Create a sub-directory app
  3. Move Main.hs there
  4. run nix-build . "" in the shell
  5. run ./result/bin/test
  6. Get the following error:
LVar left
test: 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

let
defpkgs = builtins.fetchTarball {
# Descriptive name to make the store path easier to identify
name = "nixos-22.05.1271.babb041b716";
url = "https://releases.nixos.org/nixos/22.05-small/nixos-22.05.1271.babb041b716/nixexprs.tar.xz";
# Hash obtained using `nix-prefetch-url --unpack <url>`
sha256 = "0g8vwni83zn6kgkczrm5vwmyhl473rrs9d4k4hn5gfbgfsyv7ls8";
};
config = compiler: {
packageOverrides = pkgs: rec {
haskell = pkgs.haskell // {
packages = pkgs.haskell.packages // {
"${compiler}" = pkgs.haskell.packages."${compiler}".override {
overrides = haskellPackagesNew: haskellPackagesOld: rec {
unbound-generics =
let unbound-src =
pkgs.fetchzip {
url = "https://github.com/lambdageek/unbound-generics/archive/a2a558058012b09bb313b3eb03cddb734fcf4a98.zip";
sha256 = "af4592a93d0d280591b3bcff3ebe244956cc3637bf20ed2315fb6b2e070caef4";
};
in haskellPackagesNew.callCabal2nix "unbound-generics" unbound-src {};
};
};
};
};
};
};
in
{ compiler ? "ghc902",
nixpkgs ? import defpkgs {config = (config compiler);} }:
nixpkgs.pkgs.haskell.packages."${compiler}".callCabal2nix "test" ./. {}
{-# 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
putStrLn "done"
cabal-version: 2.4
name: test
version: 0.1.0.0
-- A short (one-line) description of the package.
-- synopsis:
-- A longer description of the package.
-- description:
-- A URL where users can report bugs.
-- bug-reports:
-- The license under which the package is released.
-- license:
author: Name
maintainer: email@example.com
-- A copyright notice.
-- copyright:
-- category:
extra-source-files: CHANGELOG.md
executable test
main-is: Main.hs
-- Modules included in this executable, other than Main.
-- other-modules:
-- LANGUAGE extensions used by modules in this package.
-- other-extensions:
hs-source-dirs: app
default-language: Haskell2010
build-depends:
base >= 4 && < 5,
unbound-generics >= 0.2,
deepseq
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment