cd core/; make; cd ../
make[1]: Entering directory '/build/source/core'
ghc -O -o ./CedilleCore -Werror -rtsopts -dynamic -i./ CedilleCore.hs --make
[1 of 6] Compiling Trie             ( Trie.hs, Trie.o )
[2 of 6] Compiling Types            ( Types.hs, Types.o )
[3 of 6] Compiling Parser           ( Parser.hs, Parser.o )
[4 of 6] Compiling Norm             ( Norm.hs, Norm.o )
[5 of 6] Compiling Check            ( Check.hs, Check.o )
[6 of 6] Compiling Main             ( CedilleCore.hs, CedilleCore.o )
Linking ./CedilleCore ...
mv CedilleCore cedille-core
make[1]: Leaving directory '/build/source/core'
./create-libraries.sh
cd parser; make cedille-lexer
make[1]: Entering directory '/build/source/parser'
cd src/; alex CedilleLexer.x; mv CedilleLexer.hs ../../src;cd ..;
make[1]: Leaving directory '/build/source/parser'
cd parser; make cedille-parser
make[1]: Entering directory '/build/source/parser'
cd src/; alex CedilleLexer.x; mv CedilleLexer.hs ../../src;cd ..;
cd src/;happy CedilleParser.y; mv CedilleParser.hs ../../src;cd ..;
unused rules: 1
unused terminals: 1
shift/reduce conflicts:  1
make[1]: Leaving directory '/build/source/parser'
cd parser; make cedille-comments-lexer
make[1]: Entering directory '/build/source/parser'
cd src/; alex CedilleCommentsLexer.x; mv CedilleCommentsLexer.hs ../../src; cd ..;
make[1]: Leaving directory '/build/source/parser'
cd parser; make cedille-options-lexer
make[1]: Entering directory '/build/source/parser'
cd src/; alex CedilleOptionsLexer.x; mv CedilleOptionsLexer.hs ../../src;cd ..;
make[1]: Leaving directory '/build/source/parser'
cd parser; make cedille-options-parser
make[1]: Entering directory '/build/source/parser'
cd src/; alex CedilleOptionsLexer.x; mv CedilleOptionsLexer.hs ../../src;cd ..;
cd src/;happy CedilleOptionsParser.y; mv CedilleOptionsParser.hs ../../src;cd ..;
make[1]: Leaving directory '/build/source/parser'
cd src/templates; ghc -dynamic --make -i../ TemplatesCompiler.hs
[1 of 4] Compiling CedilleLexer     ( ../CedilleLexer.hs, ../CedilleLexer.o )
[2 of 4] Compiling CedilleTypes     ( ../CedilleTypes.hs, ../CedilleTypes.o )
[3 of 4] Compiling CedilleParser    ( ../CedilleParser.hs, ../CedilleParser.o )
[4 of 4] Compiling Main             ( TemplatesCompiler.hs, TemplatesCompiler.o )
Linking TemplatesCompiler ...
src/templates/TemplatesCompiler
Generating template MendlerSimple
Generating template Mendler
agda --library-file=libraries --library=ial --library=cedille --ghc-flag=-rtsopts  --ghc-flag=-dynamic  -c src/main.agda
Checking main (/build/source/src/main.agda).
 Checking lib (/build/source/ial/lib.agda).
  Checking datatypes (/build/source/ial/datatypes.agda).
   Checking bool (/build/source/ial/bool.agda).
    Checking level (/build/source/ial/level.agda).
   Checking bool-to-string (/build/source/ial/bool-to-string.agda).
    Checking string (/build/source/ial/string.agda).
     Checking eq (/build/source/ial/eq.agda).
     Checking char (/build/source/ial/char.agda).
      Checking nat (/build/source/ial/nat.agda).
       Checking product (/build/source/ial/product.agda).
      Checking product-thms (/build/source/ial/product-thms.agda).
       Checking unit (/build/source/ial/unit.agda).
       Checking functions (/build/source/ial/functions.agda).
     Checking list (/build/source/ial/list.agda).
      Checking maybe (/build/source/ial/maybe.agda).
      Checking empty (/build/source/ial/empty.agda).
      Checking sum (/build/source/ial/sum.agda).
   Checking integer (/build/source/ial/integer.agda).
    Checking bool-thms2 (/build/source/ial/bool-thms2.agda).
    Checking nat-thms (/build/source/ial/nat-thms.agda).
     Checking bool-thms (/build/source/ial/bool-thms.agda).
     Checking neq (/build/source/ial/neq.agda).
      Checking negation (/build/source/ial/negation.agda).
   Checking list-to-string (/build/source/ial/list-to-string.agda).
   Checking nat-division (/build/source/ial/nat-division.agda).
   Checking nat-to-string (/build/source/ial/nat-to-string.agda).
    Checking termination (/build/source/ial/termination.agda).
   Checking nat-log (/build/source/ial/nat-log.agda).
   Checking tree (/build/source/ial/tree.agda).
   Checking trie (/build/source/ial/trie.agda).
   Checking vector (/build/source/ial/vector.agda).
  Checking logic (/build/source/ial/logic.agda).
  Checking thms (/build/source/ial/thms.agda).
   Checking list-thms (/build/source/ial/list-thms.agda).
   Checking list-thms2 (/build/source/ial/list-thms2.agda).
   Checking maybe-thms (/build/source/ial/maybe-thms.agda).
   Checking string-thms (/build/source/ial/string-thms.agda).
   Checking sum-thms (/build/source/ial/sum-thms.agda).
   Checking trie-thms (/build/source/ial/trie-thms.agda).
  Checking error (/build/source/ial/error.agda).
  Checking io (/build/source/ial/io.agda).
 Checking string-format (/build/source/ial/string-format.agda).
 Checking cedille-types (/build/source/src/cedille-types.agda).
/build/source/src/cedille-types.agda:86,1-50
The backend GHC erases args so the COMPILE pragma will be ignored.
when checking the pragma COMPILE GHC args = type CedilleTypes.Args
/build/source/src/cedille-types.agda:87,1-56
The backend GHC erases opacity so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC opacity = type CedilleTypes.Opacity
/build/source/src/cedille-types.agda:89,1-50
The backend GHC erases cmds so the COMPILE pragma will be ignored.
when checking the pragma COMPILE GHC cmds = type CedilleTypes.Cmds
/build/source/src/cedille-types.agda:93,1-50
The backend GHC erases ctrs so the COMPILE pragma will be ignored.
when checking the pragma COMPILE GHC ctrs = type CedilleTypes.Ctrs
/build/source/src/cedille-types.agda:95,1-56
The backend GHC erases imports so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC imports = type CedilleTypes.Imports
/build/source/src/cedille-types.agda:101,1-54
The backend GHC erases lterms so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC lterms = type CedilleTypes.Lterms
/build/source/src/cedille-types.agda:103,1-64
The backend GHC erases maybeErased so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC maybeErased = type CedilleTypes.MaybeErased
/build/source/src/cedille-types.agda:104,1-64
The backend GHC erases forceErased so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC forceErased = type CedilleTypes.MaybeErased
/build/source/src/cedille-types.agda:105,1-62
The backend GHC erases maybeMinus so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC maybeMinus = type CedilleTypes.MaybeMinus
/build/source/src/cedille-types.agda:110,1-54
The backend GHC erases rhoHnf so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC rhoHnf = type CedilleTypes.RhoHnf
/build/source/src/cedille-types.agda:112,1-60
The backend GHC erases optPublic so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC optPublic = type CedilleTypes.OptPublic
/build/source/src/cedille-types.agda:114,1-54
The backend GHC erases params so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC params = type CedilleTypes.Params
/build/source/src/cedille-types.agda:121,1-53
The backend GHC erases cases so the COMPILE pragma will be ignored.
when checking the pragma
COMPILE GHC cases = type CedilleTypes.Cases
/build/source/src/cedille-types.agda:123,1-59
The backend GHC erases caseArgs so the COMPILE pragma will be
ignored.
when checking the pragma
COMPILE GHC caseArgs = type CedilleTypes.CaseArgs
 Checking options-types (/build/source/src/options-types.agda).
  Checking parse-tree (/build/source/src/parse-tree.agda).
 Checking cedille-options (/build/source/src/cedille-options.agda).
  Checking general-util (/build/source/src/general-util.agda).
 Checking cws-types (/build/source/src/cws-types.agda).
 Checking constants (/build/source/src/constants.agda).
 Checking json (/build/source/src/json.agda).
 Checking ctxt (/build/source/src/ctxt.agda).
  Checking ctxt-types (/build/source/src/ctxt-types.agda).
   Checking syntax-util (/build/source/src/syntax-util.agda).
  Checking subst (/build/source/src/subst.agda).
   Checking is-free (/build/source/src/is-free.agda).
   Checking rename (/build/source/src/rename.agda).
 Checking monad-instances (/build/source/src/monad-instances.agda).
 Checking process-cmd (/build/source/src/process-cmd.agda).
  Checking classify (/build/source/src/classify.agda).
   Checking conversion (/build/source/src/conversion.agda).
    Checking lift (/build/source/src/lift.agda).
     Checking erase (/build/source/src/erase.agda).
/build/source/src/conversion.agda:177,76-85
Cannot split on argument of unresolved type
_B_157 (Γ = Γ) (u = u) (t = t) (hd = hd) (tₕ = tₕ) (as = as)
(x = x) (x = x₁) (x = x₂) (x = x₃) (cs = cs) (x = x₄) (tₒ = tₒ)
(x = x₅) (x = x₆) tₓ
when checking that the pattern nas , nps has type
_B_157 (Γ = Γ) (u = u) (t = t) (hd = hd) (tₕ = tₕ) (as = as)
(x = x) (x = x₁) (x = x₂) (x = x₃) (cs = cs) (x = x₄) (tₒ = tₒ)
(x = x₅) (x = x₆) tₓ
make: *** [Makefile:141: cedille] Error 42