copilot-theorem won't install with what4-1.1, but it does with what4-1.0 #216

src/Copilot/Theorem/Kind2/Prover.hs:4:14: warning: [-Wtrustworthy-safe]

    ‘Copilot.Theorem.Kind2.Prover’ is marked as Trustworthy but has been inferred as safe!

  |

4 | {-# LANGUAGE Trustworthy #-}

  |              ^^^^^^^^^^^

[32 of 33] Compiling Copilot.Theorem.Kind2 ( src/Copilot/Theorem/Kind2.hs, /home/travis/build/Copilot-Language/copilot/dist-newstyle/build/x86_64-linux/ghc-8.8.4/copilot-theorem-3.2.1/build/Copilot/Theorem/Kind2.o )

[33 of 33] Compiling Copilot.Theorem.What4 ( src/Copilot/Theorem/What4.hs, /home/travis/build/Copilot-Language/copilot/dist-newstyle/build/x86_64-linux/ghc-8.8.4/copilot-theorem-3.2.1/build/Copilot/Theorem/What4.o )

src/Copilot/Theorem/What4.hs:218:10: error:

    • Expected kind ‘WT.BaseType -> *’,

        but ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx ::> WT.BaseRealType

                                         ::> WT.BaseRealType)’ has kind ‘*’

    • In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

      In the data declaration for ‘TransState’

    |

218 |   pow :: WB.ExprSymFn t (WB.Expr t)

    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/Copilot/Theorem/What4.hs:218:26: error:

    • Expecting one more argument to ‘WB.Expr t’

      Expected kind ‘Ctx WT.BaseType’,

        but ‘WB.Expr t’ has kind ‘WT.BaseType -> *’

    • In the second argument of ‘WB.ExprSymFn’, namely ‘(WB.Expr t)’

      In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

    |

218 |   pow :: WB.ExprSymFn t (WB.Expr t)

    |                          ^^^^^^^^^

src/Copilot/Theorem/What4.hs:219:11: error:

    • Expected kind ‘WT.BaseType’,

        but ‘EmptyCtx ::> WT.BaseRealType

             ::> WT.BaseRealType’ has kind ‘Ctx WT.BaseType’

    • In the third argument of ‘WB.ExprSymFn’, namely

        ‘(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)’

      In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

    |

219 |          (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)

    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/What4.hs:222:11: error:

    • Expected kind ‘WT.BaseType -> *’,

        but ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx ::> WT.BaseRealType

                                         ::> WT.BaseRealType)’ has kind ‘*’

    • In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

      In the data declaration for ‘TransState’

    |

222 |   logb :: WB.ExprSymFn t (WB.Expr t)

    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/Copilot/Theorem/What4.hs:222:27: error:

    • Expecting one more argument to ‘WB.Expr t’

      Expected kind ‘Ctx WT.BaseType’,

        but ‘WB.Expr t’ has kind ‘WT.BaseType -> *’

    • In the second argument of ‘WB.ExprSymFn’, namely ‘(WB.Expr t)’

      In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

    |

222 |   logb :: WB.ExprSymFn t (WB.Expr t)

    |                           ^^^^^^^^^

src/Copilot/Theorem/What4.hs:223:12: error:

    • Expected kind ‘WT.BaseType’,

        but ‘EmptyCtx ::> WT.BaseRealType

             ::> WT.BaseRealType’ has kind ‘Ctx WT.BaseType’

    • In the third argument of ‘WB.ExprSymFn’, namely

        ‘(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)’

      In the type ‘WB.ExprSymFn t (WB.Expr t) (EmptyCtx

                                               ::> WT.BaseRealType

                                               ::> WT.BaseRealType) WT.BaseRealType’

      In the definition of data constructor ‘TransState’

    |

223 |           (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)

    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

cabal: Failed to build copilot-theorem-3.2.1 (which is required by

copilot-3.2.1).

The command "cabal v2-build" exited with 1.