bogus proof for stuck type family

[codygman]

Edit: I soon found out I had a type error, but I'm guessing this bug might still be useful to know about.

I was playing around with a more granular approach to #353 and all of a sudden I got:

./granular-turtle-commands-polysemy.hs
*** Exception: bogus proof for stuck type family
CallStack (from HasCallStack):
  error, called at src/Polysemy/Plugin/Fundep.hs:178:9 in polysemy-plugin-0.2.5.0-5WyT54eXM4RG1dBfQiK6l6:Polysemy.Plugin.Fundep

Here is a reproducable script you can run with ./filename-you-saved-as.hs:

#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (ps: [ps.turtle ps.polysemy ps.polysemy-plugin])"
#! nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs-channels/archive/a84cbb60f0296210be03c08d243670dd18a3f6eb.tar.gz
-- TODO running actual script doesn't work because polysemy plugin broken in above revision, try a84cbb60f0296210be03c08d243670dd18a3f6eb
{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE BlockArguments #-}
import Polysemy
import Polysemy.Input
import Polysemy.Output
import Polysemy.Error
import Polysemy.Resource
import Polysemy.Trace
import           Turtle
import Prelude hiding (FilePath)
import qualified System.FilePath as SysFilepath

data ShellCommand m a where
  WhichCmd :: SysFilepath.FilePath -> ShellCommand m (Maybe FilePath)
  EchoCmd :: String -> ShellCommand m ()
  TestPathCmd :: SysFilepath.FilePath -> ShellCommand m Bool
  SymlinkCmd :: SysFilepath.FilePath -> ShellCommand m ()

makeSem ''ShellCommand

runShellCommandPure :: Sem (ShellCommand : r) a -> Sem r a
runShellCommandPure = interpret \case
  EchoCmd str -> pure ()
  WhichCmd str -> pure (Just $ decodeString str)
  TestPathCmd str -> pure True

runShellCommandIO :: Member (Embed IO) r => Sem (ShellCommand : r) a -> Sem r a
runShellCommandIO = interpret \case
  EchoCmd str -> embed $ putStrLn str
  WhichCmd filepath -> embed $ which (fromString filepath)

symlinkIfNotExist :: (Member Trace r, Member ShellCommand r) => FilePath -> Sem r ()
symlinkIfNotExist filepath = do
  -- whichCmd "fooooo" >>= trace . show 
  case whichCmd of
    Just filepath ->
      echoCmd "did nothing lul"
      trace "symlink already exists"
    Nothing ->
      echoCmd "did nothing lul"
      trace "symlink doesn't exist, TODO create symlink"

main :: IO ()
main = do
  putStrLn "Pure interpreter"

  putStrLn "1."
  Main.echoCmd "hi" & runShellCommandPure  & run & print 
  putStrLn ""

  putStrLn "2. The pure interpretation of whichCmd always gives Nothing"
  Main.whichCmd "nonexistent" & runShellCommandPure & run & print
  putStrLn ""

  putStrLn "3. The pure interpretation of TestPath always gives True"
  testPathCmd "nonexistent" & runShellCommandPure & run & print
  putStrLn ""


  putStrLn "4. Creates a symlink if one doesn't already exist"
  symlinkIfNotExist "nonexistent" & runShellCommandPure & runTraceList & run & print
  putStrLn ""


  
  putStrLn "Impure interpreter"

  putStrLn "1."
  Main.echoCmd "hi" & runShellCommandIO  & runM
  putStrLn ""

  putStrLn "2. Test a nonexistent command gives nothing"
  Main.whichCmd "nonexistent" & runShellCommandIO  & runM >>= print
  putStrLn ""

  putStrLn "3. Test an existing command gives Just"
  Main.whichCmd "ghc" & runShellCommandIO  & runM >>= print
  putStrLn ""

[googleson78]

When this occurs in my experience, it means that something doesn't type-check, but the plugin somehow generates the aforementioned bogus proofs and hides it. If you want to work around this you can disable the plugin, to see what's wrong, and reenable after fixing it.

But we should definitely look into this, as it's very annoying when it happens!

[tek]

for me, this mostly happens only in ghcide, but not when compiling with ghci 🤷

[codygman]

@googleson78 Yes, it was because the program wasn't typechecking this happened. I thought at first I had a valid program that Polysemy was rejecting because of a bug.