fromKnown with 3rd, 4th, ... constructor of data type

[csternagel]

It seems that fromKnown k does not work if k is not one of the first two constructors of a type. For example

$( [d| 

  data Num3 = One | Two | Three
    deriving Show

  constraint :: () -> Num3 -> Bool
  constraint () xs = True

   |] >>= compile [Cache, ImportPrelude] 
  )

allocator = fromKnown Three

result = solveAndTestP () allocator encConstraint constraint

gives me

*** Exception: Assertion failed CallStack (from HasCallStack): assert, called at /.../co4/src/CO4/Allocator.hs:131:9 in main:CO4.Allocator

while the same doesn't happen with either of fromKnown One and fromKnown Two.

[abau]

I can't reproduce this. My file Bug.hs contains:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where

import           Language.Haskell.TH (runIO)
import qualified Satchmo.Core.SAT.Minisat
import qualified Satchmo.Core.Decode 
import           CO4
import           CO4.Prelude

$( [d| 

  data Num3 = One | Two | Three
    deriving Show

  constraint :: () -> Num3 -> Bool
  constraint () xs = True

   |] >>= compile [Cache, ImportPrelude] 
  )

allocator = fromKnown Three

result = solveAndTestP () allocator encConstraint constraint

main :: IO ()
main = result >>= putStrLn . show

From CO4's top-level directory, compiling and running works:

$ stack ghc Bug.hs 
$ ./Bug 
Start producing CNF
Number of shared values: 0
Allocator: #variables: 0, #clauses: 0
Known result: valid
Abort due to known result
Nothing

Same for running in a ghci session:

$ stack ghci Bug.hs 

Warning: Couldn't find a component for file target /home/abau/projekte/co4/Bug.hs. This means that the correct ghc options might not be used.
         Attempting to load the file anyway.
Configuring GHCi with the following packages: 
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/abau/projekte/co4/Bug.hs, interpreted )
Ok, one module loaded.
Loaded GHCi configuration from /tmp/ghci2196/ghci-script
*Main> result
Start producing CNF
Number of shared values: 0
Allocator: #variables: 0, #clauses: 0
Known result: valid
Abort due to known result
Nothing

How did you run the example you've posted above?

[csternagel]

I tried both of your ways of running Bug.hs and everything worked out fine as for you. However, (strangely) when I do the following in the top-level directory of CO4, where I put Bug.hs (and incidentally that was the only way I tried to load CO4 examples up to now):

$ stack ghci
> :load Bug.hs
> result

I obtain

Start producing CNF Number of shared values: 0 *** Exception: Assertion failed CallStack (from HasCallStack): assert, called at /.../co4/src/CO4/Allocator.hs:131:9 in main:CO4.Allocator

[abau]

It seems like stack ghci Bug.hs does not check assertions, but stack ghci and :loading does. The exception was triggered by an incorrect assertion that I just removed. fromKnown should work now. Thanks for your help.