Macro type-checking: C arithmetic conversion rules

This commit generalises macro type-checking to handle C arithmetic
conversion rules as per the C standard.

What this means is that in a C expression such as

  a + b

the values 'a' and 'b' are allowed to have different types, with
implicit conversions being inserted. For example:

  - a :: CFloat, b :: CInt => convert b to CFloat before adding
  - a :: Int, b :: UInt => convert a to UInt before adding

This is achieved as follows:

  - a new package, c-expr, with the following components:

    - c-expr-core, a public sublibrary which:

        - defines standard C types and C operators,
        - implements the C arithmetic conversion rules
        - defines a collection of type-classes that can be used for
          a DSL for C arithmetic expressions
        - uses Template Haskell to define a function that can, given
          a platform, implement all the instances of these typeclasses
          for types such as CInt, CUInt, CFloat, pointers, etc

    - c-expr, the main library, which exports **platform-dependent**
      modules such as `C.Expr.Posix32` or `C.Expr.Win64` with
      type-class instances for all the C arithmetic typeclasses

    - a test-suite, which uses hsbindgen-libclang to invoke Clang on
      test programs in order to check that the implementation
      of C arithmetic conversion rules in 'c-expr-core' are
      compatible with Clang

  - the C macro typechecker imports c-expr-core, which it uses to
    compute type family reduction (e.g. the 'SubRes' type family
    which computes the return type of the subtraction operator given
    its argument types)

  - hs-bindgen generates programs that will depend on c-expr, e.g.
    to turn a C macro into a Haskell function we will generate a module
    that imports the C arithmetic operator DSL provided by c-expr

To do this, we also needed to significantly generalise the macro
typechecker:

  - Make class constraints more general by allowing what GHC calls
    FlexibleContexts and FlexibleInstances,

  - Use a special monad for constraint solving, TcSolveM.
    This monad keeps track of a work list and a set of
    inert (= fully processed) constraints.

  - Solving a constraint using a top-level instance may now add
    additional constraints to the work list.

  - Instances are keyed using a TrieMap, similar to GHC's RoughMap,
    which avoids traversing all instances when doing instance matching.

.github/workflows/haskell-ci.yml

@@ -154,6 +154,7 @@ jobs:
           echo "packages: $GITHUB_WORKSPACE/source/hs-bindgen" >> cabal.project
           echo "packages: $GITHUB_WORKSPACE/source/hs-bindgen-libclang" >> cabal.project
           echo "packages: $GITHUB_WORKSPACE/source/ansi-diff" >> cabal.project
+          echo "packages: $GITHUB_WORKSPACE/source/c-expr" >> cabal.project
           cat cabal.project
       - name: sdist
         run: |
@@ -173,14 +174,21 @@ jobs:
           echo "PKGDIR_hs_bindgen_libclang=${PKGDIR_hs_bindgen_libclang}" >> "$GITHUB_ENV"
           PKGDIR_ansi_diff="$(find "$GITHUB_WORKSPACE/unpacked" -maxdepth 1 -type d -regex '.*/ansi-diff-[0-9.]*')"
           echo "PKGDIR_ansi_diff=${PKGDIR_ansi_diff}" >> "$GITHUB_ENV"
+          PKGDIR_c_expr="$(find "$GITHUB_WORKSPACE/unpacked" -maxdepth 1 -type d -regex '.*/c-expr-[0-9.]*')"
+          echo "PKGDIR_c_expr=${PKGDIR_c_expr}" >> "$GITHUB_ENV"
           rm -f cabal.project cabal.project.local
           touch cabal.project
           touch cabal.project.local
           echo "packages: ${PKGDIR_hs_bindgen_runtime}" >> cabal.project
           echo "packages: ${PKGDIR_hs_bindgen}" >> cabal.project
           echo "packages: ${PKGDIR_hs_bindgen_libclang}" >> cabal.project
           echo "packages: ${PKGDIR_ansi_diff}" >> cabal.project
+<<<<<<< HEAD
           echo "package hs-bindgen-runtime" >> cabal.project
+=======
+          echo "packages: ${PKGDIR_c_expr}" >> cabal.project
+          echo "package hs-bindgen-patterns" >> cabal.project
+>>>>>>> ad6d31e (Macro type-checking: C arithmetic conversion rules)
           echo "    ghc-options: -Werror=missing-methods" >> cabal.project
           echo "package hs-bindgen" >> cabal.project
           echo "    ghc-options: -Werror=missing-methods" >> cabal.project
@@ -235,6 +243,8 @@ jobs:
           ${CABAL} -vnormal check
           cd ${PKGDIR_hs_bindgen_libclang} || false
           ${CABAL} -vnormal check
+          cd ${PKGDIR_c_expr} || false
+          ${CABAL} -vnormal check
           cd ${PKGDIR_ansi_diff} || false
           ${CABAL} -vnormal check
       - name: haddock

c-expr/CHANGELOG

@@ -0,0 +1,5 @@
+# Revision history for `c-expr`
+
+## 0.1.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

c-expr/LICENSE

@@ -0,0 +1,29 @@
+Copyright (c) 2024, Well-Typed LLP and Anduril Industries Inc. 
+
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of the copyright holder nor the names of its
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

c-expr/c-expr.cabal

@@ -0,0 +1,109 @@
+cabal-version:      3.0
+name:               c-expr
+version:            0.1.0.0
+license:            BSD-3-Clause
+license-file:       LICENSE
+author:             sheaf
+maintainer:         Well-Typed LLP
+category:           System
+build-type:         Simple
+extra-doc-files:    CHANGELOG.md
+tested-with:      , GHC==9.2.8
+                  , GHC==9.4.8
+                  , GHC==9.6.6
+                  , GHC==9.8.2
+                  , GHC==9.10.1
+
+common common
+  ghc-options:
+    -Wall
+    -Wno-unticked-promoted-constructors
+  default-extensions:
+    DataKinds
+    DerivingStrategies
+    FlexibleInstances
+    GADTs
+    ImportQualifiedPost
+    LambdaCase
+    MagicHash
+    MultiParamTypeClasses
+    ParallelListComp
+    StandaloneKindSignatures
+    TupleSections
+    TypeApplications
+    TypeFamilies
+    TypeOperators
+
+  build-depends:
+      base
+        >= 4.16  && < 4.21
+    , template-haskell
+        >= 2.18  && < 2.23
+    , containers
+        >= 0.6   && < 0.8
+    , directory
+        >= 1.3   && < 1.4
+    , fin
+        >= 0.3.2 && < 0.4
+    , temporary
+        >= 1.2   && < 1.4
+    , text
+        >= 1.2   && < 2.2
+    , vec
+        >= 0.5   && < 0.6
+
+-- Platform independent core library
+library c-expr-core
+
+  import:
+    common
+  visibility:
+    public
+  hs-source-dirs:
+    core
+  exposed-modules:
+    C.Type
+    C.Type.Internal.Universe
+    C.Operators
+    C.Operator.Classes
+    C.Operator.GenInstances
+  other-modules:
+    C.Operator.Internal
+    C.Operator.TH
+  default-language:
+    Haskell2010
+
+
+-- C arithmetic DSL, in the form of platform-dependent modules
+library
+  import:
+    common
+  hs-source-dirs:
+    lib
+  exposed-modules:
+    C.Expr.BuildPlatform
+    C.Expr.Posix32
+    C.Expr.Posix64
+    C.Expr.Win64
+  build-depends:
+    c-expr:c-expr-core
+  default-language:
+    Haskell2010
+
+test-suite tests
+  import:
+    common
+  hs-source-dirs:
+    test
+  main-is:
+    Main.hs
+  other-modules:
+    CallClang
+  type:
+    exitcode-stdio-1.0
+  build-depends:
+      c-expr:c-expr-core
+    , hs-bindgen-libclang
+    , hs-bindgen-runtime
+  default-language:
+    Haskell2010

c-expr/core/C/Operator/Classes.hs

@@ -0,0 +1,188 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module C.Operator.Classes
+  ( -- * Logical operators
+    Not(..)
+  , Logical(..)
+    -- * Equality and comparison
+  , RelEq(..), RelOrd(..)
+  , NotNull(..)
+    -- * Arithmetic
+    -- ** Unary
+  , Plus(..)
+  , Minus(..)
+    -- ** Binary
+  , Add(..)
+  , Sub(..)
+  , Mult(..)
+  , Div(..)
+  , Rem(..)
+    -- * Bitwise
+    -- ** Unary
+  , Complement(..)
+    -- ** Binary
+  , Bitwise(..)
+  , Shift(..)
+  ) where
+
+-- base
+import Prelude
+  ( Bool(..), Eq(..), Num(..) )
+
+import Data.Kind
+  ( Type, Constraint )
+import Foreign
+  ( Ptr, nullPtr )
+import Foreign.C
+
+--------------------------------------------------------------------------------
+
+-- | Class to compare whether a value is zero/null.
+type NotNull :: Type -> Constraint
+class NotNull a where
+  notNull :: a -> Bool
+instance ( Eq a, Num a ) => NotNull a where
+  notNull = ( /= 0 )
+instance {-# OVERLAPPING #-} NotNull ( Ptr a ) where
+  notNull = ( /= nullPtr )
+
+--------------------------------------------------------------------------------
+
+infixr 0 `not`
+-- | Class for the C logical negation operator.
+type Not :: Type -> Constraint
+class Not a where
+  -- | C logical negation operator.
+  not :: a -> CInt
+
+infixl 7 &&
+infixl 8 ||
+-- | Class for C boolean logical operators (conjunction and disjunction).
+type Logical :: Type -> Type -> Constraint
+class Logical a b where
+  (&&), (||) :: a -> b -> CInt
+
+--------------------------------------------------------------------------------
+
+infixl 5 ==
+infixl 5 !=
+-- | Class for C equality and inequality operators.
+type RelEq :: Type -> Type -> Constraint
+class RelEq a b where
+  (==), (!=) :: a -> b -> CInt
+
+infixl 4 >=
+infixl 4 <
+infixl 4 <=
+infixl 4 >
+-- | Class for C relative comparison operators (less than, greater than or equal, etc).
+type RelOrd :: Type -> Type -> Constraint
+class RelOrd a b where
+  (<=), (<), (>=), (>) :: a -> b -> CInt
+
+--------------------------------------------------------------------------------
+
+infixr 0 `plus`
+-- | Class for the C unary plus operator.
+type Plus :: Type -> Constraint
+class Plus a where
+  -- | Result type family of the C unary plus operator.
+  type family PlusRes a :: Type
+  -- | C unary plus operator.
+  plus :: a -> PlusRes a
+
+infixr 0 `negate`
+-- | Class for the C unary minus operator.
+type Minus :: Type -> Constraint
+class Minus a where
+  -- | Result type family of the C unary minus operator.
+  type family MinusRes a :: Type
+  -- | C unary plus minus.
+  negate :: a -> MinusRes a
+
+infixl 2 +
+-- | Class for the C binary addition operator.
+type Add :: Type -> Type -> Constraint
+class Add a b where
+  -- | Result type family of the C binary addition operator.
+  type family AddRes a b :: Type
+  -- | C binary addition operator.
+  (+) :: a -> b -> AddRes a b
+
+infixl 2 -
+-- | Class for the C binary subtraction operator.
+type Sub :: Type -> Type -> Constraint
+class Sub a b where
+  -- | Result type family of the C binary subtraction operator.
+  type family SubRes a b :: Type
+  -- | C binary subtraction operator.
+  (-) :: a -> b -> SubRes a b
+
+infixl 1 *
+-- | Class for the C binary multiplication operator..
+type Mult :: Type -> Type -> Constraint
+class Mult a b where
+  -- | Result type family of the C binary multiplication operator.
+  type family MultRes a b :: Type
+  -- | C binary multiplication operator.
+  (*) :: a -> b -> MultRes a b
+
+infixl 1 /
+-- | Class for the C binary division operator.
+type Div :: Type -> Type -> Constraint
+class Div a b where
+  -- | Result type family of the C binary division operator.
+  type family DivRes a b :: Type
+  -- | C binary division operator.
+  (/) :: a -> b -> DivRes a b
+
+infixl 1 %
+-- | Class for the C binary remainder operator..
+type Rem :: Type -> Type -> Constraint
+class Rem a b where
+  -- | Result type family of the C binary remainder operator.
+  type family RemRes a b :: Type
+  -- | C binary remainder operator.
+  (%) :: a -> b -> RemRes a b
+
+--------------------------------------------------------------------------------
+
+infixr 0 ~
+-- | Class for the C unary bitwise complement operator.
+type Complement :: Type -> Constraint
+class Complement a where
+  -- | Result type family of the C unary bitwise complement operator.
+  type family ComplementRes a :: Type
+  -- | C unary bitwise complement operator.
+  (~) :: a -> ComplementRes a
+
+infixl 7 .&.
+infixl 8 .|.
+infixl 6 .^.
+-- | Class for C binary bitwise logical operators.
+type Bitwise :: Type -> Type -> Constraint
+class Bitwise a b where
+  -- | Result type family of C binary bitwise logical operators.
+  type family BitsRes a b :: Type
+  -- | C binary bitwise *and* operator.
+  (.&.) :: a -> b -> BitsRes a b
+  -- | C binary bitwise *or* operator.
+  (.|.) :: a -> b -> BitsRes a b
+  -- | C binary bitwise *xor* operator.
+  (.^.) :: a -> b -> BitsRes a b
+
+infixl 3 <<
+infixl 3 >>
+-- | Class for the C binary bit-shift operators.
+type Shift :: Type -> Type -> Constraint
+class Shift a i where
+  -- | Result type family of C binary bit-shift operators.
+  type family ShiftRes a :: Type
+  -- | C binary left-shift operator.
+  (<<) :: a -> i -> ShiftRes a
+  -- | C binary right-shift operator.
+  (>>) :: a -> i -> ShiftRes a
+
+--------------------------------------------------------------------------------