uom-plugin 0.3.0.0 → 0.4.0.0

raw patch · 31 files changed

+1620/−1029 lines, 31 filesdep +QuickCheckdep +doctestdep +ghc-tcplugin-apidep −ghc-tcplugins-extradep ~basedep ~containersdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, doctest, ghc-tcplugin-api

Dependencies removed: ghc-tcplugins-extra

Dependency ranges changed: base, containers, ghc, hlint, tasty, tasty-hunit, template-haskell, units-parser

API changes (from Hackage documentation)

Files

• CHANGELOG.md +37/−0
• LICENSE +1/−1
• README.md +10/−0
• changelog +0/−24
• doc/Data/UnitsOfMeasure/Tutorial.hs +351/−0
• hlint/HLint.hs +0/−19
• package.yaml +0/−75
• src/Data/UnitsOfMeasure.hs +0/−1
• src/Data/UnitsOfMeasure/Convert.hs +19/−13
• src/Data/UnitsOfMeasure/Defs.hs +4/−1
• src/Data/UnitsOfMeasure/Internal.hs +32/−30
• src/Data/UnitsOfMeasure/Plugin.hs +172/−122
• src/Data/UnitsOfMeasure/Plugin/Convert.hs +22/−20
• src/Data/UnitsOfMeasure/Plugin/NormalForm.hs +18/−25
• src/Data/UnitsOfMeasure/Plugin/Unify.hs +37/−26
• src/Data/UnitsOfMeasure/Read.hs +2/−0
• src/Data/UnitsOfMeasure/Show.hs +0/−1
• src/Data/UnitsOfMeasure/Singleton.hs +66/−4
• src/Data/UnitsOfMeasure/Tutorial.hs +0/−171
• src/GhcApi.hs +87/−0
• src/GhcApi/Compare.hs +33/−0
• src/TcPluginExtras.hs +0/−62
• test-suite-doctest/DocTest.hs +12/−0
• test-suite-hlint/HLint.hs +19/−0
• test-suite-units/Defs.hs +51/−0
• test-suite-units/ErrorTests.hs +154/−0
• test-suite-units/Tests.hs +362/−0
• test-suite-units/Z.hs +65/−0
• tests/ErrorTests.hs +0/−120
• tests/Tests.hs +0/−278
• uom-plugin.cabal +66/−36

@@ -0,0 +1,37 @@+# Changelog++## [0.4.0.0] 2022-10-08+* Support building on GHC 9.0, 9.2 and 9.4 (thanks to Phil de Joux and Sam Derbyshire)+* Drop support for all previous versions of GHC+* Doctest the tutorial+* Various bug fixes and minor tweaks++## [0.3.0.0] 2018-07-13+### Added+* Support building on GHC 8.2 (but not yet 8.4)+* Expose toRational' in Data.UnitsOfMeasure+* An hlint test suite (thanks to Phil de Joux)+* Packaging improvements++### Fixed+* Fix unit safety bug in GHC 8.0 and later (see #22)++## [0.2.0.1] 2016-05-10+* Support building on GHC 8.0++## [0.2.0.0] 2015-12-31+### Added+* Data.UnitsOfMeasure.Read module and a Read instance for Quantity+* Make it possible to declare derived compound units+* Define litres, hectares, radians and steradians++### Fixed+* Prevent cyclic definitions of convertible units++## [0.1.1.0] 2015-11-27+### Added+* More conversion ratios (thanks to Joe Hermaszewski)+* Storable and NFData instances for Quantity (thanks to Marcin Mrotek)++## [0.1.0.0] 2015-08-19+* First public release

@@ -1,4 +1,4 @@-Copyright (c) 2014, Adam Gundry+Copyright (c) 2014-2022, Adam Gundry  All rights reserved. 

@@ -0,0 +1,10 @@+# Units of measure as a GHC type-checker plugin++:warning: This library is experimental, and may lead to unexpected type-checking failures or even type soundness bugs.++The `uom-plugin` library adds support for units of measure as a GHC type-checker plugin.  See [Data.UnitsOfMeasure.Tutorial](https://hackage.haskell.org/package/uom-plugin/docs/Data-UnitsOfMeasure-Tutorial.html) for an introduction to the library, and [the accompanying paper](http://adam.gundry.co.uk/pub/typechecker-plugins/) for more background.  An example of a package that uses the library is given in [uom-plugin-examples](https://github.com/adamgundry/uom-plugin/tree/master/uom-plugin-examples).++The latest version of the library is tested with GHC 9.0 to 9.4. Older versions of `uom-plugin` (0.3 and earlier) work with the GHC 7.10, 8.0 and 8.2 series. There are no versions supporting GHC 8.4 to 8.10 ([#43][i43]). Running `cabal haddock` on this library requires GHC 9.4 (see [#66][i66]).++[i43]: https://github.com/adamgundry/uom-plugin/issues/43+[i66]: https://github.com/adamgundry/uom-plugin/issues/66

@@ -1,24 +0,0 @@--*-change-log-*---0.3.0.0 Adam Gundry <adam@well-typed.com> June 2018-	* Support building on GHC 8.2 (but not yet 8.4)-	* Fix unit safety bug in GHC 8.0 and later (see #22)-	* Expose toRational' in Data.UnitsOfMeasure-	* Add hlint test suite (thanks to Phil de Joux)-	* Packaging improvements--0.2.0.1 Adam Gundry <adam@well-typed.com> May 2016-	* Support building on GHC 8.0--0.2.0.0 Adam Gundry <adam@well-typed.com> December 2015-	* Add Data.UnitsOfMeasure.Read module and a Read instance for Quantity-	* Make it possible to declare derived compound units-	* Define litres, hectares, radians and steradians-	* Prevent cyclic definitions of convertible units--0.1.1.0 Adam Gundry <adam@well-typed.com> November 2015-	* Add more conversion ratios (thanks to Joe Hermaszewski)-	* Add Storable and NFData instances for Quantity (thanks to Marcin Mrotek)--0.1.0.0 Adam Gundry <adam@well-typed.com> August 2015-	* First public release

@@ -0,0 +1,351 @@+{-# OPTIONS_GHC -fno-warn-unused-imports #-}++-- | This module gives a brief introduction to the @uom-plugin@+-- library.+module Data.UnitsOfMeasure.Tutorial+  (+  -- * Introduction+  -- $intro++  -- * Setup+  -- $ghc-setup++  -- * Interactive Setup+  -- $ghci-setup++  -- * The 'Unit' Kind+  -- $units++  -- * Declaring Units+  -- $decls++  -- * Creating Quantities+  -- $create++  -- ** Literals+  -- $literal++  -- ** Dimensionless Literals+  -- $dimless++  -- ** Multiplication by One+  -- $multiplication-by-one++  -- ** Attaching Units+  -- $attach++  -- ** Detaching Units+  -- $detach++  -- * Operations on Quantities+  -- $ops++  -- * Unit Polymorphism+  -- $polymorphism++  -- * Further Reading+  -- $reading+  ) where++import Data.UnitsOfMeasure++-- $setup+-- >>> import Data.UnitsOfMeasure.Defs ()++-- $intro+--+-- The @uom-plugin@ adds support for type safe units of measure. Its+-- typechecker plugin automatically solves equality constraints between units+-- of measure.++-- $ghc-setup+--+-- To use the @uom-plugin@ library, import "Data.UnitsOfMeasure" after making+-- GHC aware of the plugin and enabling language extensions.+--+-- >>> {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}+-- >>> {-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators #-}+-- >>> import Data.UnitsOfMeasure+--+-- In a module that imports the library but has not enabled the plugin or+-- enabled the required extensions you will likely get mysterious unsolved+-- constraint errors when working with units. It is only with the plugin+-- enabled that GHC can solve these.++-- $ghci-setup+--+-- To start experimenting with @uom-plugin@ in GHCi you will need to do the+-- equivalent setup.+--+-- >>> :seti -fplugin Data.UnitsOfMeasure.Plugin -XDataKinds -XQuasiQuotes -XTypeOperators+-- >>> import Data.UnitsOfMeasure++-- $units+--+-- Units of measure, such as kilograms or metres per second, are represented by+-- the abstract kind 'Unit'.  They can be built out of 'One', 'Base',+-- ('Data.UnitsOfMeasure.Internal.*:'), ('Data.UnitsOfMeasure.Internal./:') and+-- ('Data.UnitsOfMeasure.Internal.^:').  Base units are represented as+-- type-level strings (with kind 'Symbol').+--+-- >>> :kind One+-- One :: Unit+-- >>> :kind Base "m" /: Base "s"+-- Base "m" /: Base "s" :: Unit+--+-- The template Haskell quasiquoter 'u' gives a nice syntax for units (see+-- module+-- @[Text.Parse.Units](http://hackage.haskell.org/package/units-parser/docs/Text-Parse-Units.html)@+-- from the @[units-parser](http://hackage.haskell.org/package/units-parser)@+-- package for details of the syntax).  When used in a type, the quasiquoter+-- produces an expression of kind 'Unit'.+--+-- >>> :kind! [u| m^2 |]+-- [u| m^2 |] :: Unit+-- = Base "m" *: Base "m"+-- >>> :kind! [u| kg m/s |]+-- [u| kg m/s |] :: Unit+-- = (Base "kg" *: Base "m") /: Base "s"++-- $decls+--+-- Base and derived units need to be declared before use, otherwise you will+-- get unsolved constraints like @'KnownUnit' ('Unpack' ('MkUnit' "m"))@.  When+-- the TH quasiquoter 'u' is used in a declaration context, it creates new base+-- or derived units.  Alternatively, 'declareBaseUnit' and 'declareDerivedUnit'+-- can be used as top-level TH declaration splices. Where declaring new units,+-- you will also need a couple more extensions.+--+-- >>> {-# LANGUAGE TypeFamilies, UndecidableInstances #-}+--+-- > declareBaseUnit "m"+-- > declareDerivedUnit "N" "kg m / s^2"+-- > [u| kg, s |]+--+-- Note that these lines must appear in a module, not GHCi.  For+-- experimenting interactively, "Data.UnitsOfMeasure.Defs" provides+-- definitions of common units, but is subject to change.++-- $create+--+-- A numeric value @__a__@ annotated with units @__u__@ is a @'Quantity' __a__+-- __u__@. Without using the internal @'MkQuantity'@ constructor, we can use+-- literals, multiplication by 1 and unit attaching functions to create+-- quantities.++-- $literal+--+-- For literal quantities use the 'u' quasiquoter, putting the number before+-- the unit. The most general polymorphic type will be inferred.+--+-- >>> :type [u| 1 m |]+-- [u| 1 m |] :: Num a => Quantity a (Base "m")+-- >>> :type [u| 1.0 m |]+-- [u| 1.0 m |] :: Fractional a => Quantity a (Base "m")+-- >>> :type [u| 1 % 1 m |]+-- [u| 1 % 1 m |] :: Fractional a => Quantity a (Base "m")+--+-- Adding a full or partial type signature can make the underlying+-- representational type more concrete.+--+-- >>> :seti -XPartialTypeSignatures -fno-warn-partial-type-signatures+--+-- >>> :type [u| 1 m |] :: _ Int _+-- [u| 1 m |] :: _ Int _ :: Quantity Int (Base "m")+-- >>> :type [u| 1 m |] :: _ Double _+-- [u| 1 m |] :: _ Double _ :: Quantity Double (Base "m")+-- >>> :type [u| 1 m |] :: _ Rational _+-- [u| 1 m |] :: _ Rational _ :: Quantity Rational (Base "m")+--+-- Note how the 'u' quasiquoter can be used for the units in the type too. This+-- is redundant repetition with a literal but is useful when adding type+-- signatures elsewhere.+--+-- >>> [u| 1.1 m / s |] :: Quantity Double [u| m / s |]+-- [u| 1.1 m / s |]+--+-- The units parser handles various number formats.+--+-- >>> [u| 0o1327 Hz |]+-- [u| 727 s^-1 |]+-- >>> [u| 0x2d7 Hz |]+-- [u| 727 s^-1 |]+-- >>> [u| 325e-2 in |]+-- [u| 3.25 in |]+-- >>> [u| 36E+2 s |]+-- [u| 3600.0 s |]+-- >>> [u| 14.67e1 mi |]+-- [u| 146.7 mi |]++-- $dimless+--+-- Without putting the numeric value in a quotation and without templating+-- altogether we can create dimensionless units, those with units of 'One'.+--+-- >>> 1 :: Quantity Int One+-- [u| 1 |]+-- >>> [u| 1 |]+-- [u| 1 |]+-- >>> :type [u| 1 |]+-- [u| 1 |] :: Num a => Quantity a One+-- >>> :type 1 :: Quantity _ [u| 1 |]+-- 1 :: Quantity _ [u| 1 |] :: Num w => Quantity w One+-- >>> :type 1.0 :: Quantity _ One+-- 1.0 :: Quantity _ One :: Fractional w => Quantity w One+--+-- Quoted rationals are fine but type annotating them as dimensionless+-- quantities will not work.+--+-- >>> :type [u| 1 % 1 |]+-- [u| 1 % 1 |] :: Fractional a => Quantity a One+-- >>> import Data.Ratio ((%))+-- >>> :type (1 % 1) :: Quantity _ One+-- <BLANKLINE>+-- ...+-- ...Couldn't match expected type...Quantity w1 One...+-- ...with actual type...GHC.Real.Ratio...+-- ...+--+-- Things get a little weird when not being explicit about Quantity.+--+-- >>> :type 1 :: _ _ [u| 1 |]+-- 1 :: _ _ [u| 1 |]+--   :: ...+--      Num (w1 w2 One) =>+--      w1 w2 One+-- >>> :type 1 :: _ _ One+-- 1 :: _ _ One+--   :: ...+--      Num (w1 w2 One) =>+--      w1 w2 One+-- >>> :type 1.0 :: _ _ One+-- 1.0 :: _ _ One+--   :: ...+--      Fractional (w1 w2 One) =>+--      w1 w2 One++-- $multiplication-by-one+--+-- The product of a numeric value and one of a unit will attach those units to+-- the value.+--+-- >>> [u| 1 m s^-2 |] *: 9.8+-- [u| 9.8 m / s^2 |]+-- >>> 9.8 *: [u| 1 m s^-2 |]+-- [u| 9.8 m / s^2 |]+--+-- The same trick works with dimensionless values.+--+-- >>> [u| 1 m s^-2 |] *: [u| 9.8 |]+-- [u| 9.8 m / s^2 |]+-- >>> [u| 9.8 |] *: [u| 1 m s^-2 |]+-- [u| 9.8 m / s^2 |]++-- $attach+--+-- Quoted units without a value specialise to functions we can use to attach+-- units to unitless numeric values.+--+-- >>> [u| m / s^2 |] 9.8+-- [u| 9.8 m / s^2 |]+-- >>> [u| m s^-2 |] 9.8+-- [u| 9.8 m / s^2 |]+-- >>> [u| m / s / s |] 9.8+-- [u| 9.8 m / s^2 |]+-- >>> [u| s^-2 m |] 9.8+-- [u| 9.8 m / s^2 |]+--+-- Composition of these functions doesn't work as expected. It doesn't apply+-- composed units to the numeric value.+--+-- >>> [u| m |] $ [u| s^-2 |] 9.8+-- [u| [u| 9.8 s^-2 |] m |]+-- >>> [u| s^-2 |] $ [u| m |] 9.8+-- [u| [u| 9.8 m |] s^-2 |]+-- >>> [u| m |] . [u| s^-2 |] $ 9.8+-- [u| [u| 9.8 s^-2 |] m |]+-- >>> [u| s^-2 |] . [u| m |] $ 9.8+-- [u| [u| 9.8 m |] s^-2 |]+-- >>> [u| m |] [u| 9.8 s^-2 |]+-- [u| [u| 9.8 s^-2 |] m |]+-- >>> [u| s^-2 |] [u| 9.8 m |]+-- [u| [u| 9.8 m |] s^-2 |]+-- >>> [u| m |] . [u| s^-1 |] . [u| s^-1 |] $ 9.8+-- [u| [u| [u| 9.8 s^-1 |] s^-1 |] m |]++-- $detach+--+-- The underlying numeric value of a quantity may be extracted with+-- 'unQuantity', detaching the units:+--+-- >>> unQuantity [u| 15 kg |]+-- 15+-- >>> unQuantity [u| 9.8 m / s^2 |]+-- 9.8+-- >>> unQuantity <$> [[u| 1 kg |], [u| 2 kg |]]+-- [1,2]+-- >>> unQuantity . [u| kg |] <$> [1,2]+-- [1,2]+-- >>> :type unQuantity . [u| kg |]+-- unQuantity . [u| kg |] :: c -> c++-- $ops+--+-- The usual arithmetic operators from 'Num' and related typeclasses+-- are restricted to operating on dimensionless quantities.  Thus+-- using them directly on quantities with units will result in errors:+--+-- >>> 2 * [u| 5 m |]+-- <BLANKLINE>+-- ...+-- ... Couldn't match type...Base "m"...with...One...+-- ...+--+--+-- >>> [u| 2 m/s |] + [u| 5 m/s |]+-- <BLANKLINE>+-- ...+-- ... Couldn't match type...Base "m" /: Base "s"...with...One...+-- ...+--+-- Instead, "Data.UnitsOfMeasure" provides more general arithmetic+-- operators including ('+:'), ('-:'), ('*:') and ('/:').  These may+-- be used to perform unit-safe arithmetic:+--+-- >>> 2 *: [u| 5 m |]+-- [u| 10 m |]+--+-- >>> [u| 2 m / s |] +: [u| 5 m / s |]+-- [u| 7 m / s |]+--+-- However, unit errors will be detected by the type system:+--+-- >>>  [u| 3 m |] -: [u| 1 s |]+-- <BLANKLINE>+-- ...+-- ... Couldn't match type...Base "s"+-- ... with...Base "m"...+-- ...++-- $polymorphism+--+-- It is easy to work with arbitrary units (type variables of kind+-- 'Unit') rather than particular choices of unit.  The typechecker+-- plugin ensures that type inference is well-behaved and+-- automatically solves equations between units (e.g. making unit+-- multiplication commutative):+--+-- >>> let cube x = x *: x *: x+-- >>> :t cube+-- cube :: Num a => Quantity a v -> Quantity a (v *: (v *: v))+--+-- >>> let f x y = (x *: y) +: (y *: x)+-- >>> :t f+-- f :: Num a => Quantity a v -> Quantity a u -> Quantity a (u *: v)+++-- $reading+--+--  * <http://adam.gundry.co.uk/pub/typechecker-plugins/ Paper about uom-plugin>+--+--  * <https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker Plugins on the GHC wiki>

@@ -1,19 +0,0 @@-module Main (main) where--import Language.Haskell.HLint (hlint)-import System.Exit (exitFailure, exitSuccess)--arguments :: [String]-arguments =-    [ "lint"-    , "--ignore=Parse error"-    , "--ignore=Use fewer imports"  -- This is a pain for the CPP in TcPluginExtras-    , "src"-    , "tests"-    , "hlint"-    ]--main :: IO ()-main = do-    hints <- hlint arguments-    if null hints then exitSuccess else exitFailure

@@ -1,75 +0,0 @@-# This YAML file describes your package. Stack will automatically generate a-# Cabal file when you run `stack build`. See the hpack website for help with-# this file: <https://github.com/sol/hpack>.-author: Adam Gundry <adam@well-typed.com>-maintainer: Adam Gundry <adam@well-typed.com>-name: uom-plugin-synopsis: Units of measure as a GHC typechecker plugin-description: |--    The @uom-plugin@ library adds support for units of measure to GHC-    using the new experimental facility for typechecker plugins, which-    is available in GHC 7.10 and later.  See-    "Data.UnitsOfMeasure.Tutorial" for an introduction to the library.-category: Type System-license: BSD3-license-file: LICENSE-stability: experimental-github: adamgundry/uom-plugin-copyright: Copyright (c) 2014-2018, Adam Gundry-tested-with: >+-  GHC == 7.10.3,-  GHC == 8.0.2,-  GHC == 8.2.2-extra-source-files:-- package.yaml-- changelog-ghc-options:-- -Wall-- -fno-warn-unticked-promoted-constructors-library:-  dependencies:-  - base >=4.7 && <5-  - deepseq >=1.3 && <1.5-  - ghc >= 7.9 && <8.4-  - ghc-tcplugins-extra >=0.1 && <0.3-  - template-haskell >=2.9 && <2.13-  - containers >=0.5 && <0.6-  - units-parser >=0.1 && <0.2-  source-dirs: src-  exposed-modules:-  - Data.UnitsOfMeasure-  - Data.UnitsOfMeasure.Convert-  - Data.UnitsOfMeasure.Defs-  - Data.UnitsOfMeasure.Internal-  - Data.UnitsOfMeasure.Plugin-  - Data.UnitsOfMeasure.Read-  - Data.UnitsOfMeasure.Show-  - Data.UnitsOfMeasure.Singleton-  - Data.UnitsOfMeasure.Tutorial-tests:-  units:-    dependencies:-    - base-    - uom-plugin-    - tasty >=0.10 && <1.1-    - tasty-hunit >=0.9 && <0.10.1-    ghc-options:-    - -O0-    other-extensions: TemplateHaskell-    main: Tests.hs-    source-dirs:-    - tests-  hlint:-    dependencies:-    - base-    - hlint >= 1.7 && <2.2-    ghc-options:-    - -Wall-    - -O0-    - -rtsopts-    - -threaded-    - -with-rtsopts=-N-    main: HLint.hs-    source-dirs:-    - hlint-version: '0.3.0.0'

@@ -5,7 +5,6 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}  -- | See "Data.UnitsOfMeasure.Tutorial" for how to use this module.

@@ -1,18 +1,15 @@ {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}--#if __GLASGOW_HASKELL__ > 710 {-# LANGUAGE UndecidableSuperClasses #-}-#endif  {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-} @@ -73,8 +70,8 @@ import Data.UnitsOfMeasure.Internal import Data.UnitsOfMeasure.Singleton -import GHC.Exts ( Constraint )-import GHC.TypeLits+import Data.Kind (Type, Constraint)+import GHC.TypeLits (Symbol)   -- | Class to capture the dimensions to which base units belong.  For@@ -95,29 +92,35 @@  -- | Convert a unit into its canonical representation, where units are -- represented syntactically.-type family ToCBU (u :: UnitSyntax Symbol) :: Unit where+type ToCBU :: UnitSyntax Symbol -> Unit+type family ToCBU u where   ToCBU (xs :/ ys) = ListToCBU xs /: ListToCBU ys -type family ListToCBU (xs :: [Symbol]) :: Unit where+type ListToCBU :: [Symbol] -> Unit+type family ListToCBU xs where   ListToCBU '[]       = One   ListToCBU (x ': xs) = CanonicalBaseUnit x *: ListToCBU xs  -- | This constraint will be satisfied if all the base units in a -- syntactically represented unit have associated canonical -- representations.-type family HasCanonical (u :: UnitSyntax Symbol) :: Constraint where+type HasCanonical :: UnitSyntax Symbol -> Constraint+type family HasCanonical u where   HasCanonical (xs :/ ys) = (AllHasCanonical xs, AllHasCanonical ys) -type family AllHasCanonical (xs :: [Symbol]) :: Constraint where+type AllHasCanonical :: [Symbol] -> Constraint+type family AllHasCanonical xs where   AllHasCanonical '[] = ()   AllHasCanonical (x ': xs) = (HasCanonicalBaseUnit x, AllHasCanonical xs)  -- | This constraint will be satisfied if all the base units in a -- syntactically represented unit are in their canonical form.-type family IsCanonical (u :: UnitSyntax Symbol) :: Constraint where+type IsCanonical :: UnitSyntax Symbol -> Constraint+type family IsCanonical u where   IsCanonical (xs :/ ys) = (AllIsCanonical xs, AllIsCanonical ys) -type family AllIsCanonical (xs :: [Symbol]) :: Constraint where+type AllIsCanonical :: [Symbol] -> Constraint+type family AllIsCanonical xs where   AllIsCanonical '[] = ()   AllIsCanonical (x ': xs) = (CanonicalBaseUnit x ~ Base x, AllIsCanonical xs) @@ -125,6 +128,7 @@ conversionRatio :: forall proxy u . Good u                => proxy u -> Quantity Rational (u /: ToCBU (Unpack u)) conversionRatio _ = help (unitSing :: SUnit (Unpack u))+{-# INLINABLE conversionRatio #-}  help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: ToCBU u) help (SUnit xs ys) = help' xs /: help' ys@@ -149,12 +153,14 @@ -- are @v@, provided @u@ and @v@ have the same dimension. convert :: forall a u v . (Fractional a, Convertible u v) => Quantity a u -> Quantity a v convert = (ratio (undefined :: proxy' (proxy v)) (undefined :: proxy' (proxy u)) *:)+{-# INLINABLE convert #-}  -- | Calculate the conversion ratio between two units with the same -- dimension.  The slightly unusual proxy arguments allow this to be -- called using quasiquoters to specify the units, for example -- @'ratio' [u| ft |] [u| m |]@.-ratio :: forall a u v (proxy :: Unit -> *) proxy' .+ratio :: forall a u v (proxy :: Unit -> Type) proxy' .          (Fractional a, Convertible u v)       => proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v) ratio _ _ = fromRational' $ conversionRatio (undefined :: proxy u) /: conversionRatio (undefined :: proxy v)+{-# INLINABLE ratio #-}

@@ -52,4 +52,7 @@   , au = 149597870700 m |]  -- Some random other units-[u| ft = 100 % 328 m, in = 0.0254 m, mi = 1609.344 m, mph = mi/h |]+[u| ft = 100 % 328 m+  , in = 0.0254 m+  , mi = 1609.344 m+  , mph = mi/h |]

@@ -1,10 +1,9 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}@@ -68,32 +67,24 @@ data Unit  -- | Dimensionless unit (identity element)-type family One :: Unit-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type family One :: Unit where  -- | Base unit-type family Base (b :: Symbol) :: Unit-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type Base :: Symbol -> Unit+type family Base b where  -- | Multiplication for units of measure-type family (u :: Unit) *: (v :: Unit) :: Unit-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type (*:) :: Unit -> Unit -> Unit+type family u *: v where  -- | Division for units of measure-type family (u :: Unit) /: (v :: Unit) :: Unit-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type (/:) :: Unit -> Unit -> Unit+type family u /: v where  -- | Exponentiation (to a positive power) for units of measure; -- negative exponents are not yet supported (they require an Integer kind)-type family (u :: Unit) ^: (n :: Nat)  :: Unit where+type (^:) :: Unit -> Nat -> Unit+type family u ^: n where   u ^: 0 = One   u ^: 1 = u   u ^: n = u *: (u ^: (n-1))@@ -152,53 +143,65 @@ -- | Addition ('+') of quantities requires the units to match. (+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u MkQuantity x +: MkQuantity y = MkQuantity (x + y)+{-# INLINE (+:) #-}  -- | Multiplication ('*') of quantities multiplies the units. (*:) :: (Num a, w ~~ u *: v) => Quantity a u -> Quantity a v -> Quantity a w MkQuantity x *: MkQuantity y = MkQuantity (x * y)+{-# INLINE (*:) #-}  -- | Subtraction ('-') of quantities requires the units to match. (-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u MkQuantity x -: MkQuantity y = MkQuantity (x - y)+{-# INLINE (-:) #-}  -- | Negation ('negate') of quantities is polymorphic in the units. negate' :: Num a => Quantity a u -> Quantity a u negate' (MkQuantity x) = MkQuantity (negate x)+{-# INLINE negate' #-}  -- | Absolute value ('abs') of quantities is polymorphic in the units. abs' :: Num a => Quantity a u -> Quantity a u abs' (MkQuantity x) = MkQuantity (abs x)+{-# INLINE abs' #-}  -- | The sign ('signum') of a quantity gives a dimensionless result. signum' :: Num a => Quantity a u -> Quantity a One signum' (MkQuantity x) = MkQuantity (signum x)+{-# INLINE signum' #-}  -- | Convert an 'Integer' quantity into any 'Integral' type ('fromInteger'). fromInteger' :: Integral a => Quantity Integer u -> Quantity a u fromInteger' (MkQuantity x) = MkQuantity (fromInteger x)+{-# INLINE fromInteger' #-}   -- | Division ('/') of quantities divides the units. (/:) :: (Fractional a, w ~~ u /: v) => Quantity a u -> Quantity a v -> Quantity a w MkQuantity x /: MkQuantity y = MkQuantity (x / y)+{-# INLINE (/:) #-}  -- | Reciprocal ('recip') of quantities reciprocates the units. recip' :: (Fractional a, w ~~ One /: u) => Quantity a u -> Quantity a w recip' (MkQuantity x) = MkQuantity (recip x)+{-# INLINE recip' #-}  -- | Convert a 'Rational' quantity into any 'Fractional' type ('fromRational'). fromRational' :: Fractional a => Quantity Rational u -> Quantity a u fromRational' (MkQuantity x) = MkQuantity (fromRational x)+{-# INLINE fromRational' #-}  -- | Convert any 'Real' quantity into a 'Rational' type ('toRational'). toRational' :: Real a => Quantity a u -> Quantity Rational u toRational' (MkQuantity x) = MkQuantity (toRational x)+{-# INLINE toRational' #-}   -- | Taking the square root ('sqrt') of a quantity requires its units -- to be a square.  Fractional units are not currently supported. sqrt' :: (Floating a, w ~~ u ^: 2) => Quantity a w -> Quantity a u sqrt' (MkQuantity x) = MkQuantity (sqrt x)+{-# INLINE sqrt' #-}   -- | Syntactic representation of a unit as a pair of lists of base@@ -217,11 +220,13 @@ -- inverse of 'Unpack' up to the equational theory of units, but it is -- not a right inverse (because there are multiple list -- representations of the same unit).-type family Pack (u :: UnitSyntax Symbol) :: Unit where+type Pack :: UnitSyntax Symbol -> Unit+type family Pack u where   Pack (xs :/ ys) = Prod xs /: Prod ys  -- | Take the product of a list of base units.-type family Prod (xs :: [Symbol]) :: Unit where+type Prod :: [Symbol] -> Unit+type family Prod xs where   Prod '[]       = One   Prod (x ': xs) = Base x *: Prod xs @@ -237,19 +242,15 @@ -- it does not allow the structure of the unit to be observed.  The -- reduction behaviour is implemented by the plugin, because we cannot -- define it otherwise.-type family Unpack (u :: Unit) :: UnitSyntax Symbol-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type Unpack :: Unit -> UnitSyntax Symbol+type family Unpack u where   -- | This is a bit of a hack, honestly, but a good hack.  Constraints -- @u ~~ v@ are just like equalities @u ~ v@, except solving them will -- be delayed until the plugin.  This may lead to better inferred types.-type family (u :: Unit) ~~ (v :: Unit) :: Constraint-#if __GLASGOW_HASKELL__ >= 711-  where-#endif+type (~~) :: Unit -> Unit -> Constraint+type family u ~~ v where  infix 4 ~~ @@ -260,4 +261,5 @@ -- -- The instances displayed by Haddock are available only if -- "Data.UnitsOfMeasure.Defs" is imported.-type family MkUnit (s :: Symbol) :: Unit+type MkUnit :: Symbol -> Unit+type family MkUnit s

@@ -1,7 +1,4 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ > 710-{-# LANGUAGE PatternSynonyms #-}-#endif+{-# LANGUAGE DataKinds #-}  -- | This module defines a typechecker plugin that solves equations -- involving units of measure.  To use it, add@@ -15,160 +12,195 @@   ( plugin   ) where -import Plugins--import TcEvidence-import TcRnTypes-import TcType-import TcPluginM--import Coercion-import DataCon-import Type-import TyCon-import TysWiredIn--import FastString-import Outputable+import GhcApi (TcCoercion, ctEvPred, ctEvTerm, typeKind, heqDataCon, evDFunApp, dataConName, dataConWrapId, occName, occNameFS, tyConDataCons, (<+>), isWanted, isGivenCt, isGiven, UnivCoProvenance(PluginProv), mkPrimEqPred, Type(TyConApp), heqTyCon) -import OccName ( occName, occNameFS, mkTcOcc )-import Module+import qualified GHC.Plugins as Plugins+import GHC.TcPlugin.API as PluginAPI  import Data.Either-import Data.List  import Data.UnitsOfMeasure.Plugin.Convert import Data.UnitsOfMeasure.Plugin.NormalForm import Data.UnitsOfMeasure.Plugin.Unify-import TcPluginExtras -#if __GLASGOW_HASKELL__ > 710-import TyCoRep-#else-import TypeRep-#endif--import GHC.TcPluginM.Extra ( evByFiat, tracePlugin, lookupModule, lookupName )- -- | The plugin that GHC will load when this module is used with the -- @-fplugin@ option.-plugin :: Plugin-plugin = defaultPlugin { tcPlugin = const $ Just uomPlugin }+plugin :: Plugins.Plugin+plugin =+    Plugins.defaultPlugin+        { Plugins.tcPlugin = const $ Just $ PluginAPI.mkTcPlugin uomPlugin+        , Plugins.pluginRecompile = const $ pure Plugins.NoForceRecompile+        } -uomPlugin :: TcPlugin-uomPlugin = tracePlugin-                "uom-plugin"-                TcPlugin { tcPluginInit  = lookupUnitDefs-                         , tcPluginSolve = unitsOfMeasureSolver-                         , tcPluginStop  = const $ return ()-                         }+uomPlugin :: PluginAPI.TcPlugin+uomPlugin =+    PluginAPI.TcPlugin+        { PluginAPI.tcPluginInit    = lookupUnitDefs+        , PluginAPI.tcPluginSolve   = unitsOfMeasureSolver+        , PluginAPI.tcPluginRewrite = unitsOfMeasureRewrite+        , PluginAPI.tcPluginStop    = const $ return ()+        }  -unitsOfMeasureSolver :: UnitDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-unitsOfMeasureSolver uds givens _deriveds []      = do-    zonked_cts <- mapM zonkCt givens-    let (unit_givens , _) = partitionEithers $ zipWith foo givens $ map (toUnitEquality uds) zonked_cts++unitsOfMeasureSolver :: UnitDefs -> [Ct] -> [Ct] -> PluginAPI.TcPluginM PluginAPI.Solve PluginAPI.TcPluginSolveResult+unitsOfMeasureSolver uds givens []      = do+    PluginAPI.tcPluginTrace "unitsOfMeasureSolver simplifying givens" $ ppr givens+    let (unit_givens0 , _) = partitionEithers $ zipWith foo givens $ map (toUnitEquality uds) givens+    let unit_givens = filter is_useful unit_givens0     case unit_givens of-      []    -> return $ TcPluginOk [] []+      []    -> return $ PluginAPI.TcPluginOk [] []       (_:_) -> do         sr <- simplifyUnits uds $ map snd unit_givens-        tcPluginTrace "unitsOfMeasureSolver simplified givens only" $ ppr sr+        PluginAPI.tcPluginTrace "unitsOfMeasureSolver simplified givens only" $ ppr sr         case sr of-          -- Simplified tvs []    evs eqs -> TcPluginOk (map (solvedGiven . fst) unit_givens) []-          Simplified _    -> return $ TcPluginOk [] []+          -- TODO: givens simplification is currently disabled, because if we emit a given+          -- constraint like x[sk] ~ Base "kg" then GHC will "simplify" all occurrences+          -- of the type family application Base "kg" to the skolem variable x[sk].+          -- This can then result in loops as the rewriter will turn the fam app into+          -- the variable, then the plugin will "solve" it again.+          Simplified _ -> pure $ PluginAPI.TcPluginOk [] []+          Simplified ss   -> do+              -- TODO: we ought to generate evidence that depends on the+              -- previous givens (and similarly when simplifying wanteds, the+              -- evidence we generate should depend on the new wanteds).+              -- Otherwise we could potentially have a soundness issue e.g. if a+              -- GADT pattern match brings a unit equality into scope, but we+              -- later float out something that depends on it.+              let usefuls = simplifySubst ss+              xs <- mapM (substItemToCt uds) usefuls+              pure $ PluginAPI.TcPluginOk (map (solvedGiven . siCt) usefuls) xs+          -- Simplified _    -> return $ PluginAPI.TcPluginOk [] []           Impossible eq _ -> reportContradiction uds eq   where     foo :: Ct -> Either UnitEquality Ct -> Either (Ct, UnitEquality) Ct     foo ct (Left x)    = Left (ct, x)     foo _  (Right ct') = Right ct' -    -- solvedGiven ct = (ctEvTerm (ctEvidence ct), ct)+    solvedGiven ct = (ctEvTerm (ctEvidence ct), ct) +    -- TODO: if the simplify givens stage makes progress, we want to emit new+    -- givens in case GHC can substitute into constraints other than unit+    -- equalities.  However, we don't want to cause a loop by repeatedly+    -- re-simplifying the same givens.  We currently have a conservative check+    -- to see if it is useful to simplify a unit equality: if neither side of+    -- the original equality was a single variable.  There are "useful" cases+    -- this misses, however, e.g. v^2 ~ v.+    is_useful (_, ue) = isUsefulUnitEquality ue -unitsOfMeasureSolver uds givens _deriveds wanteds = do-  xs <- lookForUnpacks uds givens wanteds-  if not $ null xs then return $ TcPluginOk [] xs else do+unitsOfMeasureSolver uds givens wanteds = do     let (unit_wanteds, _) = partitionEithers $ map (toUnitEquality uds) wanteds     case unit_wanteds of-      []    -> return $ TcPluginOk [] []+      []    -> return $ PluginAPI.TcPluginOk [] []       (_:_) -> do-        (unit_givens , _) <- partitionEithers . map (toUnitEquality uds) <$> mapM zonkCt givens+        let (unit_givens , _) = partitionEithers $ map (toUnitEquality uds) givens         sr <- simplifyUnits uds unit_givens-        tcPluginTrace "unitsOfMeasureSolver simplified givens" $ ppr sr+        PluginAPI.tcPluginTrace "unitsOfMeasureSolver simplified givens" $ ppr sr+        -- TODO: it is somewhat questionable to simplify the givens again+        -- here. In principle we should be able to simplify them at the+        -- simplify-givens stage, turn them into a substitution, and have GHC+        -- apply the substitution.         case sr of           Impossible eq _ -> reportContradiction uds eq           Simplified ss   -> do sr' <- simplifyUnits uds $ map (substsUnitEquality (simplifySubst ss)) unit_wanteds-                                tcPluginTrace "unitsOfMeasureSolver simplified wanteds" $ ppr sr'+                                PluginAPI.tcPluginTrace "unitsOfMeasureSolver simplified wanteds" $ ppr sr'                                 case sr' of-                                  Impossible _eq _ -> return $ TcPluginOk [] [] -- Don't report a contradiction, see #22-                                  Simplified ss'  -> TcPluginOk [ (evMagic uds ct, ct) | eq <- simplifySolved ss', let ct = fromUnitEquality eq ]+                                  Impossible _eq _ -> return $ PluginAPI.TcPluginOk [] [] -- Don't report a contradiction, see #22+                                  Simplified ss'  -> PluginAPI.TcPluginOk [ (evMagic uds ct, ct) | eq <- simplifySolved ss', let ct = fromUnitEquality eq ]                                                          <$> mapM (substItemToCt uds) (filter (isWanted . ctEvidence . siCt) (substsSubst (simplifyUnsubst ss) (simplifySubst ss')))  -reportContradiction :: UnitDefs -> UnitEquality -> TcPluginM TcPluginResult-reportContradiction uds eq = TcPluginContradiction . pure <$> fromUnitEqualityForContradiction uds eq+reportContradiction :: UnitDefs -> UnitEquality -> PluginAPI.TcPluginM PluginAPI.Solve PluginAPI.TcPluginSolveResult+reportContradiction uds eq = PluginAPI.TcPluginContradiction . pure <$> fromUnitEqualityForContradiction uds eq  -- See #22 for why we need this-fromUnitEqualityForContradiction :: UnitDefs -> UnitEquality -> TcPluginM Ct+fromUnitEqualityForContradiction :: UnitDefs -> UnitEquality -> PluginAPI.TcPluginM PluginAPI.Solve Ct fromUnitEqualityForContradiction uds (UnitEquality ct u v) = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq _ _ -> return ct-    _ | isGivenCt ct -> newGivenCt  (ctLoc ct) (mkEqPred u' v') (mkFunnyEqEvidence (ctPred ct) u' v')-      | otherwise    -> newWantedCt (ctLoc ct) (mkEqPred u' v')+    _ | isGivenCt ct -> PluginAPI.mkNonCanonical <$> PluginAPI.newGiven  (ctLoc ct) (mkPrimEqPred u' v') (evTermToExpr (mkFunnyEqEvidence (ctPred ct) u' v'))+      | otherwise    -> PluginAPI.mkNonCanonical <$> PluginAPI.newWanted (ctLoc ct) (mkPrimEqPred u' v')   where     u' = reifyUnit uds u     v' = reifyUnit uds v  -substItemToCt :: UnitDefs -> SubstItem -> TcPluginM Ct+substItemToCt :: UnitDefs -> SubstItem -> PluginAPI.TcPluginM PluginAPI.Solve Ct substItemToCt uds si-      | isGiven (ctEvidence ct) = newGivenCt loc prd $ evByFiat "units" ty1 ty2-      | otherwise               = newWantedCt loc prd+      | isGiven (ctEvidence ct) = PluginAPI.mkNonCanonical <$> PluginAPI.newGiven loc prd (evByFiatExpr "units" ty1 ty2)+      | otherwise               = PluginAPI.mkNonCanonical <$> PluginAPI.newWanted loc prd       where-        prd  = mkEqPred ty1 ty2+        prd  = mkPrimEqPred ty1 ty2         ty1  = mkTyVarTy (siVar si)         ty2  = reifyUnit uds (siUnit si)         ct   = siCt si         loc  = ctLoc ct  -lookForUnpacks :: UnitDefs -> [Ct] -> [Ct] -> TcPluginM [Ct]-lookForUnpacks uds givens wanteds = mapM unpackCt unpacks-  where-    unpacks = concatMap collectCt $ givens ++ wanteds--    collectCt ct = collectType ct $ ctEvPred $ ctEvidence ct--    collectType ct (AppTy f s)      = collectType ct f ++ collectType ct s-    collectType ct (TyConApp tc [a])-      | tc == unpackTyCon uds       = case maybeConstant =<< normaliseUnit uds a of-                                        Just xs -> [(ct,a,xs)]-                                        _       -> []-    collectType ct (TyConApp _ as)  = concatMap (collectType ct) as-    collectType ct (FunTy t v)      = collectType ct t ++ collectType ct v-    collectType ct (ForAllTy _ t)   = collectType ct t-    collectType _  _                = [] -- TyVarTy, LitTy from 7.10, plus CastTy and CoercionTy in 8.0+{-+TODO: this leads to errors like this on GHC 9.2, but seems to work on 9.4? -    unpackCt (ct,a,xs) = newGivenCt loc (mkEqPred ty1 ty2) (evByFiat "units" ty1 ty2)-      where-        ty1 = TyConApp (unpackTyCon uds) [a]-        ty2 = mkTyConApp (unitSyntaxPromotedDataCon uds)-               [ typeSymbolKind-               , foldr promoter nil ys-               , foldr promoter nil zs ]-        loc = ctLoc ct+*** Core Lint errors : in result of Desugar (before optimization) ***+src/Data/UnitsOfMeasure/Defs.hs:19:4: warning:+    Trans coercion mis-match: (IsCanonical+                                 Univ(nominal plugin "units"+                                      :: Unpack (Base "m"), '["m"] ':/ '[]))_N+                              ; Sym (D:R:IsCanonical[0] <'["m"]>_N <'[]>_N)+      IsCanonical (Unpack (Base "m")) ~ IsCanonical ('["m"] ':/ '[])+      (AllIsCanonical '["m"], AllIsCanonical '[]) ~ IsCanonical+                                                      ('["m"] ':/ '[])+    In the RHS of $cp1HasCanonicalBaseUnit_alno :: IsCanonical+                                                     (Unpack (CanonicalBaseUnit "m"))+    In the body of letrec with binders $d(%%)_alnP :: () :: Constraint+    In the body of letrec with binders $d(%%)_alnN :: () :: Constraint+    In the body of letrec with binders $d~_alnO :: Base "m" ~ Base "m"+    In the body of letrec with binders $d(%,%)_alnM :: (Base "m"+                                                        ~ Base "m",+                                                        () :: Constraint)+    In the body of letrec with binders $d(%,%)_alnL :: ((Base "m"+                                                         ~ Base "m",+                                                         () :: Constraint),+                                                        () :: Constraint)+    Substitution: [TCvSubst+                     In scope: InScope {}+                     Type env: []+                     Co env: []]+-} -        ys = concatMap (\ (s, i) -> if i > 0 then genericReplicate i s       else []) xs-        zs = concatMap (\ (s, i) -> if i < 0 then genericReplicate (abs i) s else []) xs+unitsOfMeasureRewrite+  :: UnitDefs ->+    PluginAPI.UniqFM+        TyCon+        ([Ct] -> [Type] -> PluginAPI.TcPluginM PluginAPI.Rewrite PluginAPI.TcPluginRewriteResult)+unitsOfMeasureRewrite uds = PluginAPI.listToUFM [(unpackTyCon uds, unpackRewriter uds)] -    nil = mkTyConApp (promoteDataCon nilDataCon) [typeSymbolKind]+unpackRewriter :: UnitDefs -> [Ct] -> [Type] -> PluginAPI.TcPluginM PluginAPI.Rewrite PluginAPI.TcPluginRewriteResult+unpackRewriter uds _givens [ty] = do+  case maybeConstant =<< normaliseUnit uds ty of+    Nothing -> do PluginAPI.tcPluginTrace "unpackRewriter: no rewrite" (ppr ty)+                  pure PluginAPI.TcPluginNoRewrite+    Just u  -> do PluginAPI.tcPluginTrace "unpackRewriter: rewrite" (ppr ty <+> ppr u)+                  pure $ let reduct = reifyUnitUnpacked uds u+                         in let co = PluginAPI.mkPluginUnivCo "units" Nominal (mkTyConApp (unpackTyCon uds) [ty]) reduct+                            in PluginAPI.TcPluginRewriteTo (PluginAPI.Reduction co reduct) []+unpackRewriter _ _ tys = do+    PluginAPI.tcPluginTrace "unpackRewriter: wrong number of arguments?" (ppr tys)+    pure PluginAPI.TcPluginNoRewrite -    promoter x t = mkTyConApp cons_tycon [typeSymbolKind, mkStrLitTy x, t]-    cons_tycon = promoteDataCon consDataCon+-- TODO: the following is nonsense+lookupModule' :: PluginAPI.MonadTcPlugin m => PluginAPI.ModuleName -> p -> m PluginAPI.Module+lookupModule' modname _pkg = do+  r <- PluginAPI.findImportedModule modname PluginAPI.NoPkgQual --  (PluginAPI.OtherPkg pkg)+  case r of+    PluginAPI.Found _ md -> pure md+    _ -> do r' <- PluginAPI.findImportedModule modname PluginAPI.NoPkgQual+            case r' of+              PluginAPI.Found _ md -> pure md+              _ -> error "lookupModule: not Found"  -lookupUnitDefs :: TcPluginM UnitDefs+lookupUnitDefs :: PluginAPI.TcPluginM PluginAPI.Init UnitDefs lookupUnitDefs = do-    md <- lookupModule myModule myPackage+    md <- lookupModule' myModule myPackage     u <- look md "Unit"     b <- look md "Base"     o <- look md "One"@@ -184,11 +216,43 @@                        [d] -> promoteDataCon d                        _   -> error $ "lookupUnitDefs/getDataCon: missing " ++ s -    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)+    look md s = PluginAPI.tcLookupTyCon =<< PluginAPI.lookupOrig md (mkTcOcc s)     myModule  = mkModuleName "Data.UnitsOfMeasure.Internal"     myPackage = fsLit "uom-plugin"  +-- | Make up evidence for a fake equality constraint @t1 ~~ t2@ by coercing+-- bogus evidence of type @t1 ~ t2@.+mkFunnyEqEvidence :: Type -> Type -> Type -> EvTerm+mkFunnyEqEvidence t t1 t2 =+    castFrom `evCast'` castTo+    where+        castFrom :: EvTerm+        castFrom = evDFunApp funId tys terms+            where+                funId :: Id+                funId = dataConWrapId heqDataCon++                tys :: [Kind]+                tys = [typeKind t1, typeKind t2, t1, t2]++                terms :: [EvExpr]+                terms = [evByFiatExpr "units" t1 t2]++        castTo :: TcCoercion+        castTo =+            mkUnivCo from Representational tySource t+            where+                from :: UnivCoProvenance+                from = PluginProv "units"++                tySource :: Type+                tySource = mkHEqPred t1 t2++mkHEqPred :: Type -> Type -> Type+mkHEqPred t1 t2 = TyConApp heqTyCon [typeKind t1, typeKind t2, t1, t2]++ -- | Produce bogus evidence for a constraint, including actual -- equality constraints and our fake '(~~)' equality constraints. evMagic :: UnitDefs -> Ct -> EvTerm@@ -199,29 +263,15 @@       , tc == equivTyCon uds -> mkFunnyEqEvidence t t1 t2     _                    -> error "evMagic" --- | Make up evidence for a fake equality constraint @t1 ~~ t2@ by--- coercing bogus evidence of type @t1 ~ t2@ (or its heterogeneous--- variant, in GHC 8.0).-mkFunnyEqEvidence :: Type -> Type -> Type -> EvTerm-#if __GLASGOW_HASKELL__ >= 800-mkFunnyEqEvidence t t1 t2 = EvDFunApp (dataConWrapId heqDataCon) [typeKind t1, typeKind t2, t1, t2] [evByFiat "units" t1 t2]-                       `EvCast` mkUnivCo (PluginProv "units") Representational (mkHEqPred t1 t2) t-#else-mkFunnyEqEvidence t t1 t2 = evByFiat "units" t1 t2-                       `EvCast` TcCoercion (mkUnivCo (fsLit "units") Representational (mkTyConApp eqTyCon [typeKind t1, t1, t2]) t)-#endif---#if __GLASGOW_HASKELL__ >= 800+evByFiat :: String -> PluginAPI.TcType -> PluginAPI.TcType -> EvTerm+evByFiat s t1 t2 = PluginAPI.mkPluginUnivEvTerm s Nominal t1 t2 -#if __GLASGOW_HASKELL__ < 802-pattern FunTy :: Type -> Type -> Type-pattern FunTy t v = ForAllTy (Anon t) v-#endif+evByFiatExpr :: String -> PluginAPI.TcType -> PluginAPI.TcType -> EvExpr+evByFiatExpr s t1 t2 = evTermToExpr $ PluginAPI.mkPluginUnivEvTerm s Nominal t1 t2 -mkEqPred :: Type -> Type -> Type-mkEqPred = mkPrimEqPred+evTermToExpr :: EvTerm -> EvExpr+evTermToExpr (EvExpr e) = e+evTermToExpr _ = error "evTermToExpr" -mkHEqPred :: Type -> Type -> Type-mkHEqPred t1 t2 = TyConApp heqTyCon [typeKind t1, typeKind t2, t1, t2]-#endif+evCast' :: EvTerm -> TcCoercion -> EvTerm+evCast' = evCast . evTermToExpr

@@ -1,28 +1,17 @@-{-# LANGUAGE CPP #-} module Data.UnitsOfMeasure.Plugin.Convert   ( UnitDefs(..)   , unitKind   , isUnitKind   , normaliseUnit   , reifyUnit+  , reifyUnitUnpacked   ) where -import TyCon-import Type-#if __GLASGOW_HASKELL__ > 802-import TcType ()-#else-import TcType-#endif--#if __GLASGOW_HASKELL__ > 710-import TyCoRep-#else-import TypeRep-#endif-+import GhcApi (Type(..), typeSymbolKind, nilDataCon, consDataCon, tcSplitTyConApp_maybe, coreView, isFamilyTyCon) import Data.List +import GHC.TcPlugin.API+ import Data.UnitsOfMeasure.Plugin.NormalForm  -- | Contains references to the basic unit constructors declared in@@ -42,7 +31,7 @@  -- | 'Unit' promoted to a kind unitKind :: UnitDefs -> Kind-unitKind uds = TyConApp (promoteTyCon $ unitKindCon uds) []+unitKind uds = TyConApp (unitKindCon uds) []  -- | Is this the 'Unit' kind? isUnitKind :: UnitDefs -> Kind -> Bool@@ -89,7 +78,20 @@     reifyAtom (FamAtom f tys) = mkTyConApp f tys  -#if __GLASGOW_HASKELL__ > 710-promoteTyCon :: TyCon -> TyCon-promoteTyCon = id-#endif+-- | Convert a constant unit normal form into a type expression of kind+-- @UnitSyntax Symbol@.+reifyUnitUnpacked  :: UnitDefs -> [(BaseUnit, Integer)] -> Type+reifyUnitUnpacked uds xs =+  mkTyConApp (unitSyntaxPromotedDataCon uds)+             [ typeSymbolKind+             , foldr promoter nil ys+             , foldr promoter nil zs+             ]+  where+    ys = concatMap (\ (s, i) -> if i > 0 then genericReplicate i s       else []) xs+    zs = concatMap (\ (s, i) -> if i < 0 then genericReplicate (abs i) s else []) xs++    nil = mkTyConApp (promoteDataCon nilDataCon) [typeSymbolKind]++    promoter x t = mkTyConApp cons_tycon [typeSymbolKind, mkStrLitTy x, t]+    cons_tycon = promoteDataCon consDataCon

@@ -1,4 +1,5 @@-{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}+ module Data.UnitsOfMeasure.Plugin.NormalForm   ( Atom(..)   , BaseUnit@@ -18,6 +19,7 @@      -- * Predicates   , isOne+  , maybeSingleVariable   , isConstant   , maybeConstant   , isBase@@ -31,23 +33,17 @@   , substUnit   ) where -import Type-import TyCon-import VarSet+import Prelude hiding ((<>))+import GhcApi (elemVarSet, tyCoVarsOfType, tyCoVarsOfTypes, text, (<>))+import GhcApi.Compare (cmpType, cmpTypes, cmpTyCon, thenCmp) -import FastString-import Outputable-import Util ( thenCmp )+import GHC.TcPlugin.API  import qualified Data.Foldable as Foldable import qualified Data.Map as Map-import Data.List ( sortBy )+import Data.List ( sortOn ) import Data.Maybe-import Data.Ord -import TcPluginExtras-- -- | Base units are just represented as strings, for simplicity type BaseUnit = FastString @@ -139,6 +135,12 @@ isOne :: NormUnit -> Bool isOne = Map.null . _NormUnit +-- | Test whether a unit consists of a single variable with multiplicity 1.+maybeSingleVariable :: NormUnit -> Maybe TyVar+maybeSingleVariable x = case Map.toList (_NormUnit x) of+    [(VarAtom v, 1)] -> Just v+    _                -> Nothing+ -- | Test whether a unit is constant (contains only base literals) isConstant :: NormUnit -> Bool isConstant = all isBaseLiteral . Map.keys . _NormUnit@@ -147,7 +149,7 @@ maybeConstant :: NormUnit -> Maybe [(BaseUnit, Integer)] maybeConstant = mapM getBase . Map.toList . _NormUnit   where-    getBase (BaseAtom ty, i) = (\ b -> (b, i)) <$> isStrLitTy ty+    getBase (BaseAtom ty, i) = (, i) <$> isStrLitTy ty     getBase _                = Nothing  -- | Test whether an atom is a base unit (but not necessarily a@@ -170,14 +172,14 @@ occurs :: TyVar -> NormUnit -> Bool occurs a = any occursAtom . Map.keys . _NormUnit   where-    occursAtom (BaseAtom ty)   = elemVarSet a $ tyVarsOfType ty+    occursAtom (BaseAtom ty)   = elemVarSet a $ tyCoVarsOfType ty     occursAtom (VarAtom b)     = a == b-    occursAtom (FamAtom _ tys) = elemVarSet a $ tyVarsOfTypes tys+    occursAtom (FamAtom _ tys) = elemVarSet a $ tyCoVarsOfTypes tys   -- | View a unit as a list of atoms in order of ascending absolute exponent ascending :: NormUnit -> [(Atom, Integer)]-ascending = sortBy (comparing (abs . snd)) . Map.toList . _NormUnit+ascending = sortOn (abs . snd) . Map.toList . _NormUnit  -- | Drop a variable from a unit leftover :: TyVar -> NormUnit -> NormUnit@@ -192,12 +194,3 @@ substUnit a v u = case Map.lookup (VarAtom a) $ _NormUnit u of                     Nothing -> u                     Just i  -> (v ^: i) *: leftover a u---#if __GLASGOW_HASKELL__ > 710-tyVarsOfType :: Type -> TyCoVarSet-tyVarsOfType = tyCoVarsOfType--tyVarsOfTypes :: [Type] -> TyCoVarSet-tyVarsOfTypes = tyCoVarsOfTypes-#endif

@@ -1,3 +1,5 @@+{-# LANGUAGE DataKinds #-}+ module Data.UnitsOfMeasure.Plugin.Unify   ( SubstItem(..)   , substsSubst@@ -5,23 +7,23 @@   , UnitEquality(..)   , toUnitEquality   , fromUnitEquality+  , isUsefulUnitEquality   , SimplifyState(..)   , SimplifyResult(..)   , simplifyUnits+  , initialState   ) where -import FastString-import Name-import Outputable-import TcRnMonad ( Ct, isGiven, ctEvidence, ctEvPred )-import TcType-import Type-import Var+import GhcApi (text, (<+>), ($$), typeKind, ctEvPred, isGiven, mkSysTvName) +import GHC.TcPlugin.API as PluginAPI+import qualified GHC.TcPlugin.API.Internal as PluginAPI.Internal++import qualified GHC.Tc.Utils.Monad as GHC+import qualified GHC.Tc.Utils.TcMType as GHC+ import Data.UnitsOfMeasure.Plugin.Convert import Data.UnitsOfMeasure.Plugin.NormalForm-import TcPluginExtras-import TcPluginM   -- | A substitution is essentially a list of (variable, unit) pairs,@@ -68,34 +70,34 @@ -- | Attempt to unify two normalised units to produce a unifying -- substitution.  The 'Ct' is the equality between the non-normalised -- (and perhaps less substituted) unit type expressions.-unifyUnits :: UnitDefs -> UnitEquality -> TcPluginM UnifyResult-unifyUnits uds (UnitEquality ct u0 v0) = do tcPluginTrace "unifyUnits" (ppr u0 $$ ppr v0)+unifyUnits :: UnitDefs -> UnitEquality -> PluginAPI.TcPluginM PluginAPI.Solve UnifyResult+unifyUnits uds (UnitEquality ct u0 v0) = do PluginAPI.tcPluginTrace "unifyUnits" (ppr u0 $$ ppr v0)                                             unifyOne uds ct [] [] [] (u0 /: v0) -unifyOne :: UnitDefs -> Ct -> [TyVar] -> TySubst -> TySubst -> NormUnit -> TcPluginM UnifyResult+unifyOne :: UnitDefs -> Ct -> [TyVar] -> TySubst -> TySubst -> NormUnit -> PluginAPI.TcPluginM PluginAPI.Solve UnifyResult unifyOne uds ct tvs subst unsubst u       | isOne u           = return $ Win tvs subst unsubst       | isConstant u      = return   Lose-      | otherwise         = tcPluginTrace "unifyOne" (ppr u) >> go [] (ascending u)+      | otherwise         = {- tcPluginTrace "unifyOne" (ppr u) >> -} go [] (ascending u)        where-        go :: [(Atom, Integer)] -> [(Atom, Integer)] -> TcPluginM UnifyResult+        go :: [(Atom, Integer)] -> [(Atom, Integer)] -> PluginAPI.TcPluginM PluginAPI.Solve UnifyResult         go _  []                       = return $ Draw tvs subst unsubst         go ls (at@(VarAtom a, i) : xs) = do-            tch <- if given_mode then return True else isTouchableTcPluginM a+            tch <- if given_mode then return True else PluginAPI.isTouchableTcPluginM a             let r = divideExponents (-i) $ leftover a u             case () of                 () | tch && divisible i u -> return $ if occurs a r then Draw tvs subst unsubst                                                                     else Win tvs (extendSubst (SubstItem a r ct) subst) unsubst-                   | tch && any (not . isBase . fst) xs -> do beta <- newUnitVar+                   | tch && not (all (isBase . fst) xs) -> do beta <- newUnitVar                                                               let subst'   = extendSubst (SubstItem a    (varUnit beta *: r) ct) subst                                                                   unsubst' = extendSubst (SubstItem beta (varUnit a    /: r) ct) unsubst                                                               unifyOne uds ct (beta:tvs) subst' unsubst' $ substUnit a (varUnit beta *: r) u                    | otherwise            -> go (at:ls) xs          go ls (at@(FamAtom f tys, i) : xs) = do-          mb <- matchFam f tys-          case normaliseUnit uds . snd =<< mb of+          mb <- PluginAPI.matchFam f tys+          case normaliseUnit uds . PluginAPI.reductionReducedType =<< mb of             Just v  -> unifyOne uds ct tvs subst unsubst $ mkNormUnit (ls ++ xs) *: v ^: i             Nothing -> go (at:ls) xs         go ls (at@(BaseAtom  _, _) : xs) = go (at:ls) xs@@ -103,15 +105,16 @@          given_mode = isGiven (ctEvidence ct) -        newUnitVar | given_mode = newSkolemTyVar $ unitKind uds-                   | otherwise  = newFlexiTyVar  $ unitKind uds+        newUnitVar | given_mode = PluginAPI.Internal.unsafeLiftTcM $ newSkolemTyVar $ unitKind uds+                   | otherwise  = PluginAPI.Internal.unsafeLiftTcM $ GHC.newFlexiTyVar  $ unitKind uds          newSkolemTyVar kind = do-            x <- newUnique+            x <- GHC.newUnique             let name = mkSysTvName x (fsLit "beta")-            return $ mkTcTyVar name kind vanillaSkolemTv+            return $ PluginAPI.mkTyVar name kind -- mkTcTyVar name kind vanillaSkolemTv  + data UnitEquality = UnitEquality Ct NormUnit NormUnit  instance Outputable UnitEquality where@@ -135,6 +138,14 @@ fromUnitEquality (UnitEquality ct _ _) = ct  +isUsefulUnitEquality :: UnitEquality -> Bool+isUsefulUnitEquality (UnitEquality _ lhs rhs) =+    case (maybeSingleVariable lhs, maybeSingleVariable rhs) of+        (Nothing, Nothing) -> True+        (Just v, _)        -> occurs v rhs+        (_, Just v)        -> occurs v lhs++ data SimplifyState   = SimplifyState { simplifyFreshVars :: [TyVar]                   , simplifySubst     :: TySubst@@ -163,14 +174,14 @@   ppr (Simplified ss)     = text "Simplified" $$ ppr ss   ppr (Impossible eq eqs) = text "Impossible" <+> ppr eq <+> ppr eqs -simplifyUnits :: UnitDefs -> [UnitEquality] -> TcPluginM SimplifyResult-simplifyUnits uds eqs0 = tcPluginTrace "simplifyUnits" (ppr eqs0) >> simples initialState eqs0+simplifyUnits :: UnitDefs -> [UnitEquality] -> PluginAPI.TcPluginM PluginAPI.Solve SimplifyResult+simplifyUnits uds eqs0 = PluginAPI.tcPluginTrace "simplifyUnits" (ppr eqs0) >> simples initialState eqs0   where-    simples :: SimplifyState -> [UnitEquality] -> TcPluginM SimplifyResult+    simples :: SimplifyState -> [UnitEquality] -> PluginAPI.TcPluginM PluginAPI.Solve SimplifyResult     simples ss [] = return $ Simplified ss     simples ss (eq:eqs) = do         ur <- unifyUnits uds (substsUnitEquality (simplifySubst ss) eq)-        tcPluginTrace "unifyUnits result" (ppr ur)+        PluginAPI.tcPluginTrace "unifyUnits result" (ppr ur)         case ur of           Win  tvs subst unsubst -> let (ss', xs) = win eq tvs subst unsubst ss                                     in simples ss' (xs ++ eqs)

@@ -4,6 +4,8 @@ {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} {-# OPTIONS_GHC -fno-warn-orphans #-} 

@@ -4,7 +4,6 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}  {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-}

@@ -1,6 +1,5 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-}@@ -76,12 +75,75 @@   | normaliseUnitSyntax (forgetSUnit su) == normaliseUnitSyntax (forgetSUnit sv) = Just (unsafeCoerce Refl)   | otherwise = Nothing --- | Calculate a normal form of a syntactic unit: a map from base unit--- names to non-zero integers.+-- | Calculate a normal form of a syntactic unit: a map from base unit names to+-- non-zero integers.+--+-- >>> normaliseUnitSyntax ([] :/ [])+-- fromList []+--+-- >>> normaliseUnitSyntax (["m"] :/ [])+-- fromList [("m",1)]+--+-- >>> normaliseUnitSyntax (["m", "m"] :/ [])+-- fromList [("m",2)]+--+-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ [])+-- fromList [("m",3)]+--+-- >>> normaliseUnitSyntax ([] :/ ["m"])+-- fromList [("m",-1)]+--+-- >>> normaliseUnitSyntax ([] :/ ["m", "m"])+-- fromList [("m",-2)]+--+-- >>> normaliseUnitSyntax ([] :/ ["m", "m", "m"])+-- fromList [("m",-3)]+--+-- >>> normaliseUnitSyntax (["m"] :/ ["m"])+-- fromList []+--+-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m"])+-- fromList [("m",1)]+--+-- >>> normaliseUnitSyntax (["m"] :/ ["m", "m"])+-- fromList [("m",-1)]+--+-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m", "m"])+-- fromList []+--+-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ ["m", "m"])+-- fromList [("m",1)]+--+-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m", "m", "m"])+-- fromList [("m",-1)]+--+-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ ["m", "m", "m"])+-- fromList []+--+-- >>> normaliseUnitSyntax (replicate 3 "m" :/ [])+-- fromList [("m",3)]+--+-- >>> normaliseUnitSyntax ([] :/ replicate 3 "m")+-- fromList [("m",-3)]+--+-- >>> normaliseUnitSyntax (replicate 3 "m" :/ replicate 3 "m")+-- fromList []+--+-- >>> normaliseUnitSyntax (["m"] :/ ["s"])+-- fromList [("m",1),("s",-1)]+--+-- >>> normaliseUnitSyntax (["m"] :/ ["s", "s"])+-- fromList [("m",1),("s",-2)]+--+-- >>> normaliseUnitSyntax (["m", "m"] :/ []) == normaliseUnitSyntax (["m", "m"] :/ ["m", "m"])+-- False+--+-- >>> normaliseUnitSyntax (["m"] :/ []) == normaliseUnitSyntax (["m"] :/ ["m", "m"])+-- False normaliseUnitSyntax :: UnitSyntax String -> Map.Map String Integer normaliseUnitSyntax (xs :/ ys) =     Map.filter (/= 0)-        (foldl' (\ m x -> Map.insertWith (-) x 1 m)+        (foldl' (\ m x -> Map.insertWith (+) x (negate 1) m)             (foldl' (\ m x -> Map.insertWith (+) x 1 m) Map.empty xs) ys)  

@@ -1,171 +0,0 @@--- | This module gives a brief introduction to the @uom-plugin@--- library.--{-# OPTIONS_GHC -fno-warn-unused-imports #-}-module Data.UnitsOfMeasure.Tutorial-  ( -- $tutorial-  ) where--import Data.UnitsOfMeasure---- $tutorial------ === Prerequisites------ To use the @uom-plugin@ library, simply import "Data.UnitsOfMeasure"--- and pass the option @-fplugin Data.UnitsOfMeasure.Plugin@ to GHC, for--- example by adding the following above the module header of your source--- files:------ > {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}------ This will enable the typechecker plugin, which automatically solves--- equality constraints between units of measure.  You will also need--- some language extensions:------ > {-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators #-}------ In order to declare new units, you will need:------ > {-# LANGUAGE TypeFamilies, UndecidableInstances #-}--------- === Interactive use------ If experimenting with @uom-plugin@ in GHCi you will need to--- activate the plugin with the command------ >>> :seti -fplugin Data.UnitsOfMeasure.Plugin------ otherwise you will get mysterious unsolved constraint errors.  You--- will probably also need the extensions:------ >>> :seti -XDataKinds -XQuasiQuotes -XTypeOperators--------- === The 'Unit' kind------ Units of measure, such as kilograms or metres per second, are--- represented by the abstract kind 'Unit'.  They can be built out of--- 'One', 'Base', ('Data.UnitsOfMeasure.Internal.*:'),--- ('Data.UnitsOfMeasure.Internal./:') and--- ('Data.UnitsOfMeasure.Internal.^:').  Base units are represented as--- type-level strings (with kind 'Symbol').  For example,------ >>> :kind One--- One :: Unit------ >>> :kind Base "m" /: Base "s"--- Base "m" /: Base "s" :: Unit------ The TH quasiquoter 'u' is provided to give a nice syntax for units--- (see @Text.Parse.Units@ from the @units-parser@ package for details--- of the syntax).  When used in a type, the quasiquoter produces an--- expression of kind 'Unit', for example------ >>> :kind! [u| m^2 |]--- [u| m^2 |] :: Unit--- = Base "m" ^: 2------ >>> :kind! [u| kg m/s |]--- [u|kg m/s|] :: Unit--- = (Base "kg" *: Base "m") /: Base "s"--------- === Declaring base and derived units------ Base and derived units need to be declared before use, otherwise--- you will get unsolved constraints like @'KnownUnit' ('Unpack' ('MkUnit' "m"))@.--- When the TH quasiquoter 'u' is used as in a declaration context, it--- creates new base or derived units.  Alternatively,--- 'declareBaseUnit' and 'declareDerivedUnit' can be used as top-level--- TH declaration splices.  For example:------ > declareBaseUnit "m"--- > declareDerivedUnit "N" "kg m / s^2"--- > [u| kg, s |]------ Note that these lines must appear in a module, not GHCi.  For--- experimenting interactively, "Data.UnitsOfMeasure.Defs" provides--- definitions of common units, but is subject to change.--------- === Creating quantities------ A 'Quantity' is a numeric value annotated with its units.--- Quantities can be created using the 'u' quasiquoter in an--- expression, for example @[u| 5 m |]@ or @[u| 2.2 m/s^2 |]@.  The--- syntax consists of an integer or decimal number, followed by a--- unit.------ The type of a quantity includes the underlying representation type and--- the unit, for example:------ > [u| 5 m |] :: Quantity Int (Base "m")------ or using the 'u' quasiquoter in the type as well:------ > [u| 1.1 m/s |] :: Quantity Double [u| m/s |]------ Numeric literals may be used to produce dimensionless quantities--- (i.e. those with unit 'One'):------ > 2 :: Quantity Int One------ The underlying numeric value of a quantity may be extracted with--- 'unQuantity':------ >>> unQuantity [u| 15 kg |]--- 15--------- === Operations on quantities------ The usual arithmetic operators from 'Num' and related typeclasses--- are restricted to operating on dimensionless quantities.  Thus--- using them directly on quantities with units will result in errors:------ >>> 2 * [u| 5 m |]---   Couldn't match type ‘Base "m"’ with ‘One’...------ >>> [u| 2 m/s |] + [u| 5 m/s |]---   Couldn't match type ‘Base "m" /: Base "s"’ with ‘One’...------ Instead, "Data.UnitsOfMeasure" provides more general arithmetic--- operators including ('+:'), ('-:'), ('*:') and ('/:').  These may--- be used to perform unit-safe arithmetic:------ >>> 2 *: [u| 5 m |]--- [u| 10 m |]------ >>> [u| 2 m / s |] +: [u| 5 m / s |]--- [u| 7 m / s |]------ However, unit errors will be detected by the type system:------ >>>  [u| 3 m |] -: [u| 1 s |]---   Couldn't match type ‘Base "s"’ with ‘Base "m"’...--------- === Unit polymorphism------ It is easy to work with arbitrary units (type variables of kind--- 'Unit') rather than particular choices of unit.  The typechecker--- plugin ensures that type inference is well-behaved and--- automatically solves equations between units (e.g. making unit--- multiplication commutative):------ >>> let cube x = x *: x *: x--- >>> :t cube--- cube :: Num a => Quantity a v -> Quantity a (v ^: 3)------ >>> let f x y = (x *: y) +: (y *: x)--- >>> :t f--- f :: Num a => Quantity a v -> Quantity a u -> Quantity a (u *: v)--------- == Further reading------  * <http://adam.gundry.co.uk/pub/typechecker-plugins/ Paper about uom-plugin>------  * <https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker Plugins on the GHC wiki>

@@ -0,0 +1,87 @@+{-# LANGUAGE CPP #-}++module GhcApi+    ( module X+    ) where++import GHC.Core.Coercion as X (mkUnivCo, Coercion)++import GHC.Core.DataCon as X (dataConName, promoteDataCon, dataConWrapId)+import GHC.Data.FastString as X (FastString(..), fsLit)+import GHC as X (mkModuleName)+import GHC.Types.Name as X (mkSysTvName)+import GHC.Types.Name.Occurrence as X (occName, occNameFS, mkTcOcc)+import GHC.Utils.Outputable as X (Outputable(..), (<>), (<+>), ($$), text)+import GHC.Driver.Plugins as X (Plugin(..), defaultPlugin)++import GHC.Tc.Types.Evidence as X+    ( EvTerm(..)+    , TcCoercion+    , TcCoercionR+    , EvExpr+    , evCast+    , evDFunApp+    )++import GHC.Tc.Plugin as X+    ( TcPluginM+    , tcPluginTrace, matchFam, newFlexiTyVar, isTouchableTcPluginM+    , tcLookupTyCon, zonkCt+    , newUnique+    )+-- import GHC.Tc.Types as X (TcPlugin(..), TcPluginResult(..))+import GHC.Tc.Types.Constraint as X+    ( Ct(..), CtLoc+    , ctLoc, ctEvidence, ctEvPred, ctPred, ctEvExpr, ctEvTerm+    , isGiven, isWanted, isGivenCt+    , mkNonCanonical+    )+import GHC.Tc.Utils.TcType as X (tcSplitTyConApp_maybe {-, vanillaSkolemTv -})+import GHC.Core.TyCon as X (TyCon(..), Role(..), isFamilyTyCon, tyConDataCons)++import GHC.Core.TyCo.Rep as X+    ( UnivCoProvenance(PluginProv)+    , Kind+    , Type(TyConApp, TyVarTy, AppTy, ForAllTy, FunTy, LitTy)+    , mkTyVarTy+    , mkFunTy+#if __GLASGOW_HASKELL__ > 900+    , cmpTyLit+#endif+    )++import GHC.Core.Coercion as X (mkPrimEqPred)+import GHC.Core.Predicate as X+    ( EqRel(..)+    , Pred(..)+    , classifyPredType+    )+import GHC as X (PredType)+import GHC.Core.Type as X+    ( splitTyConApp_maybe, typeKind+    , tyCoVarsOfType, tyCoVarsOfTypes+    , mkNumLitTy, mkTyConApp+    , isNumLitTy, isStrLitTy+    , coreView+    , mkStrLitTy+    , nonDetCmpType, nonDetCmpTypes, nonDetCmpTc+    , mkAppTy+    )++import GHC.Builtin.Types as X (typeSymbolKind, nilDataCon, consDataCon, heqTyCon, heqDataCon)++import GHC.Types.Unique as X+    ( getUnique+    , nonDetCmpUnique+    )++import GHC.Types.Var as X+    ( TyVar+    , DFunId+    , Id+    , mkTcTyVar+    )++import GHC.Types.Var.Set as X (TyCoVarSet, elemVarSet)++import GHC.Driver.Plugins as X (PluginRecompile(..))

@@ -0,0 +1,33 @@+{-# LANGUAGE CPP #-}++module GhcApi.Compare+  ( cmpType+  , cmpTypes+  , cmpTyCon+  , thenCmp+  ) where++import GhcApi++import GHC.Utils.Misc (thenCmp)++-- TODO: all this is deeply dodgy!  These comparison functions are+-- non-deterministic, so we may end up getting different results on different+-- runs.  Really we should replace them with deterministic versions.++cmpTyCon :: TyCon -> TyCon -> Ordering+cmpTyCon = nonDetCmpTc++cmpType :: Type -> Type -> Ordering+#if __GLASGOW_HASKELL__ > 900+cmpType (LitTy x) (LitTy y) = cmpTyLit x y+cmpType t1 t2 = nonDetCmpType t1 t2+#else+cmpType = nonDetCmpType+#endif++cmpTypes :: [Type] -> [Type] -> Ordering+cmpTypes [] [] = EQ+cmpTypes (t1:ts1) (t2:ts2) = cmpType t1 t2 `thenCmp` cmpTypes ts1 ts2+cmpTypes [] _ = LT+cmpTypes _ [] = GT

@@ -1,62 +0,0 @@-{-# LANGUAGE CPP #-}--module TcPluginExtras-  ( -- * Wrappers-    newUnique-  , newWantedCt-  , newGivenCt--    -- * GHC API changes-  , cmpType-  , cmpTypes-  , cmpTyCon-  ) where--import TcEvidence ( EvTerm )-import TcRnTypes  ( mkNonCanonical )-import TcRnMonad  ( Ct, CtLoc )-import Type       ( PredType )-import TyCon      ( TyCon )--import GHC.TcPluginM.Extra--#if __GLASGOW_HASKELL__ < 711-import Unique     ( Unique )-import qualified TcRnMonad-import TcPluginM ( TcPluginM, unsafeTcPluginTcM )-#else-import TcPluginM ( TcPluginM, newUnique )-#endif--#if __GLASGOW_HASKELL__ < 802-import Type ( cmpType, cmpTypes )-#else-import Type ( Type, nonDetCmpType, nonDetCmpTypes )-import Unique ( getUnique, nonDetCmpUnique )-#endif---#if __GLASGOW_HASKELL__ < 711-newUnique :: TcPluginM Unique-newUnique = unsafeTcPluginTcM TcRnMonad.newUnique-#endif--newWantedCt :: CtLoc -> PredType -> TcPluginM Ct-newWantedCt loc = fmap mkNonCanonical . newWanted loc--newGivenCt :: CtLoc -> PredType -> EvTerm -> TcPluginM Ct-newGivenCt loc prd ev = mkNonCanonical <$> newGiven loc prd ev--#if __GLASGOW_HASKELL__ < 802-cmpTyCon :: TyCon -> TyCon -> Ordering-cmpTyCon = compare-#else-cmpType :: Type -> Type -> Ordering-cmpType = nonDetCmpType--cmpTypes :: [Type] -> [Type] -> Ordering-cmpTypes = nonDetCmpTypes--cmpTyCon :: TyCon -> TyCon -> Ordering-cmpTyCon a b = getUnique a `nonDetCmpUnique` getUnique b-#endif

@@ -0,0 +1,12 @@+module Main (main) where++import Test.DocTest (doctest)++arguments :: [String]+arguments =+    [ "-isrc"+    , "src/Data/UnitsOfMeasure/Singleton.hs"+    ]++main :: IO ()+main = doctest arguments

@@ -0,0 +1,19 @@+module Main (main) where++import Language.Haskell.HLint (hlint)+import System.Exit (exitFailure, exitSuccess)++arguments :: [String]+arguments =+    [ "lint"+    , "--ignore=Parse error"+    , "--ignore=Use fewer imports"  -- This is a pain for the CPP in TcPluginExtras+    , "src"+    , "test-suite-units"+    , "test-suite-hlint"+    ]++main :: IO ()+main = do+    hints <- hlint arguments+    if null hints then exitSuccess else exitFailure

@@ -0,0 +1,51 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Defs where++import Data.UnitsOfMeasure+import Data.UnitsOfMeasure.Defs ()++-- Declarations.+declareBaseUnit "byte"+declareDerivedUnit "bps" "byte / s"+declareConvertibleUnit "kilobyte" 1024 "byte"+declareConvertibleUnit "squiggle" 2 "m/s"++-- This declares a dimensionless unit that requires explicit conversion.+[u| dime = 1 1 |]+dime :: Fractional a => Quantity a [u|dime|] -> Quantity a [u|1|]+dime = convert+++try :: Quantity Double [u| ft^3 m^3 |]+try = convert [u| 2 l^2  |]++++{-++-- These tests demonstrate the need for simplification of givens.  This doesn't+-- currently work, however.++type family F (u :: Unit)++thingy :: (x *: y ~ Base "m") => proxy x y -> F x -> F (Base "m" /: y)+thingy _ x = x++thingy2 :: (x *: x ~ x) => proxy x -> F x -> F One+thingy2 _ x = x++thingy3 :: (x *: x ~ x *: x *: x) => proxy x -> F x -> F One+thingy3 _ x = x++-}

@@ -0,0 +1,154 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}++{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}++#if __GLASGOW_HASKELL__ > 710+{-# OPTIONS_GHC -fno-warn-deferred-type-errors #-}+#endif++module ErrorTests where++import Data.UnitsOfMeasure+import Data.UnitsOfMeasure.Defs ()++import GHC.TypeLits++mismatch1 :: Quantity Double [u| s/m |]+mismatch1 = [u| 3 m/s |]++mismatch1_errors :: [[String]]+mismatch1_errors = couldn'tMatchErrors "Base \"m\" /: Base \"s\"" "Base \"s\" /: Base \"m\""++mismatch2 :: Quantity Int [u| s |]+mismatch2 = [u| 2 m |] +: ([u| 2 s |] :: Quantity Int [u| s |])++mismatch2_errors :: [[String]]+mismatch2_errors = couldn'tMatchErrors "Base \"s\"" "Base \"m\""++couldn'tMatchErrors :: String -> String -> [[String]]+couldn'tMatchErrors t1 t2 =+    [ [ "Couldn't match type ‘" ++ t1 ++ "’", "with ‘" ++ t2 ++ "’" ]+    , [ "Couldn't match type ‘" ++ t2 ++ "’", "with ‘" ++ t1 ++ "’" ]+    , [ "Couldn't match type: " ++ t1, "with: " ++ t2 ]+    , [ "Couldn't match type: " ++ t2, "with: " ++ t1 ]+    ]+++given1 :: ((One *: a) ~ (a *: One)) => Quantity Double a -> Quantity Double [u|kg|]+given1 = id++given1_errors :: [[String]]+given1_errors = [ [ "Could not deduce (a ~ Base \"kg\")"+                  , "from the context ((One *: a) ~ (a *: One))" ]+                , [ "Could not deduce (Base \"kg\" ~ a)"+                  , "from the context: (One *: a) ~ (a *: One)" ]+                , [ "Could not deduce: a ~ Base \"kg\""+                  , "from the context: (One *: a) ~ (a *: One)" ]+                , [ "Could not deduce: Base \"kg\" ~ a"+                  , "from the context: (One *: a) ~ (a *: One)" ]+                ]+++given2 :: ((One *: a) ~ (b *: One)) => Quantity Double a -> Quantity Double [u|kg|]+given2 = id++given2_errors :: [[String]]+given2_errors = [ [ "Could not deduce (a ~ Base \"kg\")"+                  , "from the context ((One *: a) ~ (b *: One))" ]+                , [ "Could not deduce (Base \"kg\" ~ a)"+                  , "from the context: (One *: a) ~ (b *: One)" ]+                , [ "Could not deduce: a ~ Base \"kg\""+                  , "from the context: (One *: a) ~ (b *: One)" ]+                , [ "Could not deduce: Base \"kg\" ~ a"+                  , "from the context: (One *: a) ~ (b *: One)" ]+                ]+++given3 :: ((a ^: 2) ~ (b ^: 3)) => Quantity Integer b -> Quantity Integer a+given3 _ = [u| 3 s |]++given3_errors :: [[String]]+given3_errors = [ [ "Could not deduce (a ~ Base \"s\")"+                  , "from the context ((a ^: 2) ~ (b ^: 3))" ]+                , [ "Could not deduce (Base \"s\" ~ a)"+                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]+                , [ "Could not deduce: a ~ Base \"s\""+                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]+                , [ "Could not deduce: Base \"s\" ~ a"+                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]+                ]++op_a1 :: Quantity Double [u| m |]+op_a1 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))++op_a2 :: Quantity Double [u| m |]+op_a2 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))++op_a3 :: Quantity Double [u| m |]+op_a3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))++op_b1 :: Quantity Int [u| m |]+op_b1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))++op_b2 :: Quantity Int [u| m |]+op_b2 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))++op_b3 :: Quantity Int [u| m |]+op_b3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))++op_c1 :: Quantity Integer [u| m |]+op_c1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))++op_c2 :: Quantity Integer [u| m |]+op_c2 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))++op_c3 :: Quantity Integer [u| m |]+op_c3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))++op_d1 :: Quantity Rational [u| m |]+op_d1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))++op_d2 :: Quantity Rational [u| m |]+op_d2 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))++op_d3 :: Quantity Rational [u| m |]+op_d3 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))++opErrors :: String -> String -> String -> [[String]]+opErrors a b c = matchErrors a b c "One" ++ matchErrors a b c "(Base \"m\")"++matchErrors :: String -> String -> String -> String -> [[String]]+matchErrors a b c d =+#if __GLASGOW_HASKELL__ >= 900+  [ [ "Couldn't match type ‘" ++ a ++ "’ with ‘" ++ b ++ "’"+    , "Actual: Quantity " ++ c ++ " " ++ d+    ]+  , [ "Couldn't match type ‘" ++ a ++ "’ with ‘" ++ b ++ "’"+    , "Expected: Quantity " ++ c ++ " " ++ d+    ]+  , [ "Couldn't match type ‘" ++ b ++ "’ with ‘" ++ a ++ "’"+    , "Expected: Quantity " ++ c ++ " " ++ d+    ]+  , [ "Couldn't match type ‘" ++ b ++ "’ with ‘" ++ a ++ "’"+    , "Actual: Quantity " ++ c ++ " " ++ d+    ]+  , [ "Couldn't match type: " ++ a, "with: " ++ b+    , "Actual: Quantity " ++ c ++ " " ++ d+    ]+  ]+#else+  [ [ "Couldn't match type ‘" ++ b ++ "’ with ‘" ++ a ++ "’"+    ]+  ]+#endif+++exponentDoesn'tDistribute :: Quantity Double ([u| m |] ^: (x + y)) -> Quantity Double (([u| m |] ^: x) *: [u| m |] ^: y)+exponentDoesn'tDistribute x = x

@@ -0,0 +1,362 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}++-- WARNING: It would be a lot of work to add type annotations to avoid type-default+-- warnings and what is more this leads to type checking failures;+--+-- {-# LANGUAGE PartialTypeSignatures #-}+--+--   , testGroup "read normalisation"+--     [ testCase "1 m/m"+--         $ (read "[u| 1 m/m |]" :: _ Integer _) @?= [u| 1 |]+--     , testCase "-0.3 m s^-1"+--         $ (read "[u| -0.3 m s^-1 |]" :: _ Double _) @?= [u| -0.3 m/s |]+--     , testCase "42 s m s"+--         $ (read "[u| 42 s m s |]" :: _ Integer _)  @?= [u| 42 m s^2 |]+--     ]+--+-- > cabal new-repl uom-plugin:units+-- solveSimpleWanteds: too many iterations (limit = 4)+{-# OPTIONS_GHC -fno-warn-type-defaults #-}++module Main+    ( main++    -- * Exported to avoid -Wunused-top-binds.+    , attract+    , foo+    , foo'+    , angularSpeed+    , associativity+    , commutativity+    , unit+    , inverse+    , inverse2+    , f+    , g+    , givens+    , givens2+    , givens3+    , baz+    , baf+    , patternSplice+    , pow+    , dimensionless+    ) where++import Data.UnitsOfMeasure+import Data.UnitsOfMeasure.Convert+import Data.UnitsOfMeasure.Defs ()+import Data.UnitsOfMeasure.Show++import Control.Monad (unless)+import Control.Exception+import Data.List+import Data.Ratio ((%))++import Test.Tasty+import Test.Tasty.HUnit++import Defs ()+import ErrorTests+import Z (z)+import qualified Z (tests)++-- Some basic examples++myMass :: Quantity Double (Base "kg")+myMass = [u| 65 kg |]++gravityOnEarth :: Quantity Double [u| m/s^2 |]+gravityOnEarth = [u| 9.808 m/(s*s) |]++readMass :: Read a => String -> Quantity a (Base "kg")+readMass = fmap [u| kg |] read++forceOnGround :: Quantity Double [u| N |]+forceOnGround = gravityOnEarth *: myMass++inMetresPerSecond :: a -> Quantity a [u| m/s |]+inMetresPerSecond = [u| m/s |]++attract+    :: Fractional a+    => Quantity a [u| kg |]+    -> Quantity a [u| kg |]+    -> Quantity a [u| m |]+    -> Quantity a [u| N |]+attract+    (m1 :: Quantity a [u| kg |])+    (m2 :: Quantity a [u| kg |])+    (r :: Quantity a [u| m |])+    = _G *: m1 *: m2 /: (r *: r) :: Quantity a [u| N |]+  where+    _G = [u| 6.67384e-11 N*m^2/kg^2 |]++sum' :: [Quantity Double u] -> Quantity Double u+sum' = foldr (+:) zero++mean :: [Quantity Double u] -> Quantity Double u+mean xs = sum' xs /: mk (genericLength xs)++foo :: Num a => Quantity a u -> Quantity a v -> Quantity a (u *: v)+foo x y = x *: y +: y *: x++foo' :: Num a => Quantity a u -> Quantity a v -> Quantity a (u *: v)+foo' = foo++-- thanks to expipiplus1, https://github.com/adamgundry/uom-plugin/issues/14+angularSpeed :: Quantity Rational [u|rad/s|]+angularSpeed = z x+  where x :: Quantity Rational [u|s^-1|]+        x = undefined+++-- Check that the abelian group laws hold++associativity :: Quantity a (u *: (v *: w)) -> Quantity a ((u *: v) *: w)+associativity = id++commutativity :: Quantity a (u *: v) -> Quantity a (v *: u)+commutativity = id++unit :: Quantity a (u *: One) -> Quantity a u+unit = id++inverse :: Quantity a (u *: (One /: u)) -> Quantity a One+inverse = id++inverse2 :: proxy b -> Quantity a (Base b /: Base b) -> Quantity a One+inverse2 _ = id+++-- Gingerly now...++-- w^-2 ~ kg^-2  =>  w ~ kg+f :: (One /: (w ^: 2)) ~ (One /: [u| kg^2 |])  => Quantity a w -> Quantity a [u| kg |]+f = id++-- u ~ v * w, v^2 ~ v  =>  u ~ w+g :: (u ~ (v *: w), (v ^: 2) ~ v) => Quantity a u -> Quantity a w+g = id++-- a*a ~ 1  =>  a ~ 1+givens :: ((a *: a) ~ One) => Quantity Double a -> Quantity Double One+givens = id++-- a^2 ~ b^3, b^6 ~ 1 => a ~ 1+givens2 :: ((a ^: 2) ~ (b ^: 3), (b ^: 6) ~ One) => Quantity Double a -> Quantity Double One+givens2 = id++-- a^2 ~ b^3, b^37 ~ 1 => b ~ 1+givens3 :: ((a ^: 2) ~ (b ^: 3), (b ^: 37) ~ One) => Quantity Double b -> Quantity Double One+givens3 = id++-- in baf, c is uniquely determined to be a^3 (or b^2)+baz :: (a ~ (c ^: 3), b ~ (c ^: 2)) => Quantity Double a -> Quantity Double b -> Quantity Double c -> Int+baz _ _ _ = 3+baf :: ((a ^: 2) ~ (b ^: 3)) => Quantity Double a -> Quantity Double b -> Int+baf qa qb = baz qa qb undefined+++-- Miscellaneous bits and bobs++-- Pattern splices are supported, albeit with restricted types+patternSplice :: Quantity Integer [u| m |] -> Quantity Rational [u| kg/s |] -> Bool+patternSplice [u| 2 m |] [u| 0.0 kg / s |] = True+patternSplice [u| 1 m |] [u| 0.1 kg / s |] = True+patternSplice _          _                 = False++-- Andrew's awkward generalisation example is accepted only with a+-- type signature, even with NoMonoLocalBinds+tricky+    :: forall a u . Num a+    => Quantity a u+    -> (Quantity a (u *: Base "m"), Quantity a (u *: Base "kg"))+tricky x =+    let h :: Quantity a v -> Quantity a (u *: v)+        h = (x *:)+    in (h [u| 3 m |], h [u| 5 kg |])+++-- Test that basic constraints involving exponentiation work+pow :: Quantity a (u *: (v ^: i)) -> Quantity a ((v ^: i) *: u)+pow = id+++-- This declares a synonym for One+[u| dimensionless = 1 |]+dimensionless :: Quantity a [u|dimensionless|] -> Quantity a [u|1|]+dimensionless = id+++-- Runtime testsuite++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "uom-plugin"+  [ testGroup "Get the underlying value with unQuantity"+    [ testCase "unQuantity 3 m"                $ unQuantity [u| 3 m |]            @?= 3+    , testCase "unQuantity 3 s^2"              $ unQuantity [u| 3 s^2 |]          @?= 3+#if __GLASGOW_HASKELL__ > 802+    -- TODO: Find out why unQuantity (3 m s^-1) fails with ghc-8.0.2.+    -- solveSimpleWanteds: too many iterations (limit = 4)+    , testCase "unQuantity 3 m s^-1"           $ unQuantity [u| 3 m s^-1 |]       @?= 3+#endif+    , testCase "unQuantity 3.0 kg m^2 / m s^2" $ unQuantity [u| 3.0 kg m / s^2 |] @?= 3+    , testCase "unQuantity 1"                  $ unQuantity (mk 1)                @?= 1+    , testCase "unQuantity 1 (1/s)"            $ unQuantity [u| 1 (1/s) |]        @?= 1+    , testCase "unQuantity 1 1/s"              $ unQuantity [u| 1 1/s |]          @?= 1+    , testCase "unQuantity 1 s^-1"             $ unQuantity [u| 1 s^-1 |]         @?= 1+    , testCase "unQuantity 2 1 / kg s"         $ unQuantity [u| 2 1 / kg s |]     @?= 2+    , testCase "unQuantity (1 % 2) kg"         $ unQuantity [u| 1 % 2 kg |]       @?= 0.5+    ]+  , testGroup "Attach units by applying the quasiquoter without a numeric value"+    [ testCase "m 3"                           $ [u| m |] 3           @?= [u| 3 m |]+    , testCase "m <$> [3..5]"                  $ [u| m |] <$> [3..5]  @?= [[u| 3 m |],[u| 4 m |],[u| 5 m |]]+    , testCase "m/s 3"                         $ [u| m/s |] 3         @?= [u| 3 m/s |]+#if __GLASGOW_HASKELL__ > 802+    -- TODO: Find out why (m s^-1 3) fails with ghc-8.0.2.+    -- solveSimpleWanteds: too many iterations (limit = 4)+    , testCase "m s^-1 3"                      $ [u| m s^-1 |] 3      @?= [u| 3 m s^-1 |]+#endif+    , testCase "s^2 3"                         $ [u| s^2 |] 3         @?= [u| 3 s^2 |]+    , testCase "1 $ 3"                         $ [u|dimensionless|] 3 @?= [u| 3 |]+    , testCase "fmap [u| kg |] read $ \"3\""   $ readMass "3"         @?= [u| 3 kg |]+    , testCase "fmap [u| kg |] read $ \"3.0\"" $ readMass "3"         @?= [u| 3.0 kg |]+    ]+  , testGroup "Showing constants"+    [ testCase "show 3m"                 $ show [u| 3 m |]                @?= "[u| 3 m |]"+    , testCase "show 3m/s"               $ show [u| 3 m/s |]              @?= "[u| 3 m / s |]"+    , testCase "show 3.2 s^2"            $ show [u| 3.2 s^2 |]            @?= "[u| 3.2 s^2 |]"+    , testCase "show 3.0 kg m^2 / m s^2" $ show [u| 3.0 kg m^2 / m s^2 |] @?= "[u| 3.0 kg m / s^2 |]"+    , testCase "show 1"                  $ show (mk 1)                    @?= "[u| 1 |]"+    , testCase "show 1 s^-1"             $ show [u| 1 s^-1 |]             @?= "[u| 1 s^-1 |]"+    , testCase "show 2 1 / kg s"         $ show [u| 2 1 / kg s |]         @?= "[u| 2 kg^-1 s^-1 |]"+    , testCase "show (1 % 2) kg"         $ show [u| 1 % 2 kg |]           @?= "[u| 0.5 kg |]"+    ]+  , testGroup "Basic operations"+    [ testCase "2 + 2"                   $ [u| 2 s |] +: [u| 2 s |]        @?= [u| 4 s |]+    , testCase "in m/s"                  $ inMetresPerSecond 5             @?= [u| 5 m/s |]+    , testCase "mean"                    $ mean [ [u| 2 N |], [u| 4 N |] ] @?= [u| 3 N |]+    , testCase "tricky generalisation"   $ tricky [u| 2 s |]               @?= ([u| 6 m s |], [u| 10 kg s |])+    , testCase "polymorphic zero"        $ [u| 0 |] @?= [u| 0 m |]+    , testCase "polymorphic frac zero"   $ [u| 0.0 |] @?= [u| 0.0 N / m |]+    ]+  , testGroup "Literal 1 (*:) Quantity _ u"+    [ testCase "_ = Double"+        $ 1 *: ([u| 1 m |] :: (Quantity Double (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Int"+        $ 1 *: ([u| 1 m |] :: (Quantity Int (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Integer"+        $ 1 *: ([u| 1 m |] :: (Quantity Integer (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Rational, 1 *: [u| 1 m |]"+        $ 1 *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Rational, mk (1 % 1) *: [u| 1 m |]"+        $ mk (1 % 1) *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Rational, 1 *: [u| 1 % 1 m |]"+        $ 1 *: ([u| 1 % 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Rational, mk (1 % 1) *: [u| 1 % 1 m |]"+        $ mk (1 % 1) *: ([u| 1 % 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]+    ]+  , testGroup "(1 :: Quantity _ One) (*:) Quantity _ u"+    [ testCase "_ = Double"+        $ (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Double (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Int"+        $ (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Int (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Integer"+        $ (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Integer (Base "m"))) @?= [u| 1 m |]+    , testCase "_ = Int"+        $ (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]+    ]+  , testGroup "errors when a /= b, (1 :: Quantity a One) (*:) Quantity b u"+    [ testGroup "b = Double"+      [ testCase "a = Int" $ op_a1 `throws` opErrors "Double" "Int" "Int"+      , testCase "a = Integer" $ op_a2 `throws` opErrors "Double" "Integer" "Integer"+      , testCase "a = Rational" $ op_a3 `throws` opErrors "Double" "GHC.Real.Ratio Integer" "Rational"+      ]+    , testGroup "b = Int"+      [ testCase "a = Double" $ op_b1 `throws` opErrors "Int" "Double" "Double"+      , testCase "a = Integer" $ op_b2 `throws` opErrors "Int" "Integer" "Integer"+      , testCase "a = Rational" $ op_b3 `throws` opErrors "Int" "GHC.Real.Ratio Integer" "Rational"+      ]+    , testGroup "b = Integer"+      [ testCase "a = Double" $ op_c1 `throws` opErrors "Integer" "Double" "Double"+      , testCase "a = Int" $ op_c2 `throws` opErrors "Integer" "Int" "Int"+      , testCase "a = Rational" $ op_c3 `throws` opErrors "Integer" "GHC.Real.Ratio Integer" "Rational"+      ]+    , testGroup "b = Rational"+      [ testCase "a = Double" $ op_d1 `throws` opErrors "GHC.Real.Ratio Integer" "Double" "Double"+      , testCase "a = Int" $ op_d2 `throws` opErrors "GHC.Real.Ratio Integer" "Int" "Int"+      , testCase "a = Integer" $ op_d3 `throws` opErrors "GHC.Real.Ratio Integer" "Integer" "Integer"+      ]+    ]+  , testGroup "showQuantity"+    [ testCase "myMass"         $ showQuantity myMass         @?= "65.0 kg"+    , testCase "gravityOnEarth" $ showQuantity gravityOnEarth @?= "9.808 m / s^2"+    , testCase "forceOnGround"  $ showQuantity forceOnGround  @?= "637.52 kg m / s^2"+    ]+  , testGroup "convert"+    [ testCase "10m in ft"     $ convert [u| 10m |]   @?= [u| 32.8 ft |]+    , testCase "5 km^2 in m^2" $ convert [u| 5km^2 |] @?= [u| 5000000 m m |]+    , testCase "ratio"         $ show (ratio [u| ft |] [u| m |]) @?= "[u| 3.28 ft / m |]"+    , testCase "100l in m^3"   $ convert [u| 100l |]   @?= [u| 0.1 m^3 |]+    , testCase "1l/m in m^2"   $ convert [u| 1l/m |]   @?= [u| 0.001 m^2 |]+    , testCase "1l/m in m^2"   $ convert [u| 1l/m |]   @?= [u| 0.001 m^2 |]+    , testCase "5l in ft^3"    $ convert [u| 5l   |]   @?= [u| 0.17643776 ft^3 |]+    , testCase "2000000l^2 in ft^3 m^3" $ convert [u| 2000000l^2 |] @?= [u| 70.575104 ft^3 m^3 |]+    , testCase "42 rad/s in s^-1" $ convert [u| 42 rad/s |] @?= [u| 42 s^-1 |]+    , testCase "2.4 l/h in m" $ convert [u| 2.4 l/ha |] @?= [u| 2.4e-7 m |]+    , testCase "1 m^4 in l m" $ convert [u| 1 m^4 |] @?= [u| 1000 l m |]+    ]+  , Z.tests+  , testGroup "errors"+    [ testCase "s/m ~ m/s"            $ mismatch1 `throws` mismatch1_errors+    , testCase "m + s"                $ mismatch2 `throws` mismatch2_errors+    , testCase "a ~ a  =>  a ~ kg"    $ given1 undefined `throws` given1_errors+    , testCase "a ~ b  =>  a ~ kg"    $ given2 undefined `throws` given2_errors+    , testCase "a^2 ~ b^3  =>  a ~ s" $ given3 undefined `throws` given3_errors+    , testCase "a^(x + y) ~ a^x a^y"  $ exponentDoesn'tDistribute undefined `throws` matchErrors "Base \"m\" ^: (x + y)" "(Base \"m\" ^: x) *: (Base \"m\" ^: y)" "Double" "(MkUnit \"m\" ^: (x + y))"+    ]+  , testGroup "read . show"+    [ testCase "3 m"     $ read (show [u| 3 m     |]) @?= [u| 3 m     |]+    , testCase "1.2 m/s" $ read (show [u| 1.2 m/s |]) @?= [u| 1.2 m/s |]+    , testCase "0"       $ read (show [u| 1       |]) @?= [u| 1       |]+    ]+  , testGroup "read normalisation"+    [ testCase "1 m/m"       $ read "[u| 1 m/m |]"       @?= [u| 1 |]+    , testCase "-0.3 m s^-1" $ read "[u| -0.3 m s^-1 |]" @?= [u| -0.3 m/s |]+    , testCase "42 s m s"    $ read "[u| 42 s m s |]"    @?= [u| 42 m s^2 |]+    ]+  , testGroup "read equality (avoid false equivalences)"+    [ testCase "1 m/m^2 /= 1 m" $+        (read "[u| 1 m/m^2 |]" :: Quantity Double [u| m |]) `throws` noParse++    , testCase "1 m /= 1 m/m^2" $+        (read "[u| 1 m |]" :: Quantity Double [u| m/m^2 |]) `throws` noParse+    ]+  ]++-- | Assert that evaluation of the first argument (to WHNF) will throw+-- an exception whose string representation contains one of the given+-- lists of substrings.+throws :: a -> [[String]] -> Assertion+throws v xs =+    (evaluate v >> assertFailure "No exception!") `catch` \ (e :: SomeException) ->+        unless (any (all (`isInfixOf` show e)) xs) $+          assertFailure ("Expected:\n" ++ unlines (concat xs) ++ "\nbut got:\n" ++ show e)++noParse :: [[String]]+noParse = [["Prelude.read: no parse"]]

@@ -0,0 +1,65 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}++module Z (z, tests) where++import Test.Tasty+import Test.Tasty.HUnit++import Data.UnitsOfMeasure (Quantity, u)+import Data.UnitsOfMeasure.Convert (Convertible, convert)+import Data.UnitsOfMeasure.Defs ()+++-- Inferring this type used to lead to unit equations with occur-check+-- failures, because it involves things like Pack (Unpack u) ~ u+-- The type signature is intentionally left off here to check that the+-- compiler can infer it.+-- z :: forall a (u :: Unit) (v :: Unit). (Fractional a, Convertible u v)+--   => Quantity a u+--   -> Quantity a v+{-# ANN z "HLint: ignore Eta reduce" #-}+z q = convert q+++#if __GLASGOW_HASKELL__ >= 902+newtype A a = A a+newtype B a = B a++  -- See https://github.com/adamgundry/uom-plugin/pull/86.  This code works in GHC+-- 9.2 and later because they do not flatten, but is broken in 9.0 because of+-- flattening. For now we skip testing it in 9.0.  In principle we should be+-- able to fix it by having simplify-givens do substitution.+instance (Convertible u [u| m |], q ~ Quantity Double u) => Show (A q) where+    show (A x) = show y+        where+            y :: Quantity Double [u| m |]+            y = convert x++instance (q ~ Quantity Double [u| m |]) => Show (B q) where+    show (B x) = show y+        where+            y :: Quantity Double [u| m |]+            y = convert x++tests :: TestTree+tests = testGroup "show via convert"+    [ testCase "A 1.01km" $ show (A [u| 1.01 km |]) @?= "[u| 1010.0 m |]"+    , testCase "B 1010m" $ show (B [u| 1010.0 m |]) @?= "[u| 1010.0 m |]"+    ]+++#else+tests :: TestTree+tests = testGroup "show via convert" []+#endif

@@ -1,120 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE QuasiQuotes #-}--{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}--#if __GLASGOW_HASKELL__ > 710-{-# OPTIONS_GHC -fno-warn-deferred-type-errors #-}-#endif--module ErrorTests where--import Data.UnitsOfMeasure-import Data.UnitsOfMeasure.Defs--mismatch1 :: Quantity Double [u| s/m |]-mismatch1 = [u| 3 m/s |]--mismatch1_errors = [ [ "Couldn't match type ‘Base \"s\" /: Base \"m\"’"-                     , "with ‘Base \"m\" /: Base \"s\"’" ]-                   , [ "Couldn't match type ‘Base \"m\" /: Base \"s\"’"-                     , "with ‘Base \"s\" /: Base \"m\"’" ]-                   ]---mismatch2 = [u| 2 m |] +: ([u| 2 s |] :: Quantity Int [u| s |])--mismatch2_errors = [ [ "Couldn't match type ‘Base \"s\"’ with ‘Base \"m\"’" ]-                   , [ "Couldn't match type ‘Base \"m\"’ with ‘Base \"s\"’" ]-                   ]---given1 :: ((One *: a) ~ (a *: One)) => Quantity Double a -> Quantity Double [u|kg|]-given1 = id--given1_errors = [ [ "Could not deduce (a ~ Base \"kg\")"-                  , "from the context ((One *: a) ~ (a *: One))" ]-                , [ "Could not deduce: a ~ Base \"kg\""-                  , "from the context: (One *: a) ~ (a *: One)" ]-                , [ "Could not deduce: Base \"kg\" ~ a"-                  , "from the context: (One *: a) ~ (a *: One)" ]-                ]---given2 :: ((One *: a) ~ (b *: One)) => Quantity Double a -> Quantity Double [u|kg|]-given2 = id--given2_errors = [ [ "Could not deduce (a ~ Base \"kg\")"-                  , "from the context ((One *: a) ~ (b *: One))" ]-                , [ "Could not deduce: a ~ Base \"kg\""-                  , "from the context: (One *: a) ~ (b *: One)" ]-                , [ "Could not deduce: Base \"kg\" ~ a"-                  , "from the context: (One *: a) ~ (b *: One)" ]-                ]---given3 :: ((a ^: 2) ~ (b ^: 3)) => Quantity Integer b -> Quantity Integer a-given3 _ = [u| 3 s |]--given3_errors = [ [ "Could not deduce (a ~ Base \"s\")"-                  , "from the context ((a ^: 2) ~ (b ^: 3))" ]-                , [ "Could not deduce: a ~ Base \"s\""-                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]-                , [ "Could not deduce: Base \"s\" ~ a"-                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]-                ]--op_a1 :: Quantity Double [u| m |]-op_a1 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))--op_a2 :: Quantity Double [u| m |]-op_a2 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))--op_a3 :: Quantity Double [u| m |]-op_a3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Double (Base "m")))--op_b1 :: Quantity Int [u| m |]-op_b1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))--op_b2 :: Quantity Int [u| m |]-op_b2 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))--op_b3 :: Quantity Int [u| m |]-op_b3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Int (Base "m")))--op_c1 :: Quantity Integer [u| m |]-op_c1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))--op_c2 :: Quantity Integer [u| m |]-op_c2 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))--op_c3 :: Quantity Integer [u| m |]-op_c3 = (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Integer (Base "m")))--op_d1 :: Quantity Rational [u| m |]-op_d1 = (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))--op_d2 :: Quantity Rational [u| m |]-op_d2 = (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))--op_d3 :: Quantity Rational [u| m |]-op_d3 = (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Rational (Base "m")))--opErrors :: String -> String -> String -> [[String]]-opErrors a b c =-#if __GLASGOW_HASKELL__ > 710 -  [ [ "Couldn't match type ‘" ++ a ++ "’ with ‘" ++ b ++ "’"-    , "Expected type: Quantity " ++ c ++ " (Base \"m\")"-    ]-  ]-#else-  [ [ "Couldn't match type ‘" ++ b ++ "’ with ‘" ++ a ++ "’"-    ]-  ]-#endif

@@ -1,278 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}--import Data.UnitsOfMeasure-import Data.UnitsOfMeasure.Convert-import Data.UnitsOfMeasure.Internal (fromRational')-import Data.UnitsOfMeasure.Defs ()-import Data.UnitsOfMeasure.Show--import Control.Monad (unless)-import Control.Exception-import Data.List-import Data.Ratio ((%))-import GHC.Real (Ratio(..))--import Test.Tasty-import Test.Tasty.HUnit--import ErrorTests----- Declarations-declareBaseUnit "byte"-declareDerivedUnit "bps" "byte / s"-declareConvertibleUnit "kilobyte" 1024 "byte"-declareConvertibleUnit "squiggle" 2 "m/s"----- Some basic examples--myMass :: Quantity Double (Base "kg")-myMass = [u| 65 kg |]--gravityOnEarth :: Quantity Double [u| m/s^2 |]-gravityOnEarth = [u| 9.808 m/(s*s) |]--forceOnGround :: Quantity Double [u| N |]-forceOnGround = gravityOnEarth *: myMass--inMetresPerSecond :: a -> Quantity a [u| m/s |]-inMetresPerSecond = [u| m/s |]--attract (m1 :: Quantity a [u| kg |]) (m2 :: Quantity a [u| kg |]) (r :: Quantity a [u| m |])-    = _G *: m1 *: m2 /: (r *: r) :: Quantity a [u| N |]-  where-    _G = [u| 6.67384e-11 N*m^2/kg^2 |]--sum' = foldr (+:) zero-mean xs = sum' xs /: mk (genericLength xs)--foo x y = x *: y +: y *: x--foo' :: Num a => Quantity a u -> Quantity a v -> Quantity a (u *: v)-foo' = foo---- thanks to expipiplus1, https://github.com/adamgundry/uom-plugin/issues/14-angularSpeed :: Quantity Rational [u|rad/s|]-angularSpeed = convert x-  where x :: Quantity Rational [u|s^-1|]-        x = undefined----- Check that the abelian group laws hold--associativity :: Quantity a (u *: (v *: w)) -> Quantity a ((u *: v) *: w)-associativity = id--commutativity :: Quantity a (u *: v) -> Quantity a (v *: u)-commutativity = id--unit :: Quantity a (u *: One) -> Quantity a u-unit = id--inverse :: Quantity a (u *: (One /: u)) -> Quantity a One-inverse = id--inverse2 :: proxy b -> Quantity a (Base b /: Base b) -> Quantity a One-inverse2 _ = id----- Gingerly now...---- w^-2 ~ kg^-2  =>  w ~ kg-f :: (One /: (w ^: 2)) ~ (One /: [u| kg^2 |])  => Quantity a w -> Quantity a [u| kg |]-f = id---- u ~ v * w, v^2 ~ v  =>  u ~ w-g :: (u ~ (v *: w), (v ^: 2) ~ v) => Quantity a u -> Quantity a w-g = id---- a*a ~ 1  =>  a ~ 1-givens :: ((a *: a) ~ One) => Quantity Double a -> Quantity Double One-givens = id---- a^2 ~ b^3, b^6 ~ 1 => a ~ 1-givens2 :: ((a ^: 2) ~ (b ^: 3), (b ^: 6) ~ One) => Quantity Double a -> Quantity Double One-givens2 = id---- a^2 ~ b^3, b^37 ~ 1 => b ~ 1-givens3 :: ((a ^: 2) ~ (b ^: 3), (b ^: 37) ~ One) => Quantity Double b -> Quantity Double One-givens3 = id---- in baf, c is uniquely determined to be a^3 (or b^2)-baz :: (a ~ (c ^: 3), b ~ (c ^: 2)) => Quantity Double a -> Quantity Double b -> Quantity Double c -> Int-baz _ _ _ = 3-baf :: ((a ^: 2) ~ (b ^: 3)) => Quantity Double a -> Quantity Double b -> Int-baf qa qb = baz qa qb undefined----- Miscellaneous bits and bobs---- Inferring this type used to lead to unit equations with occur-check--- failures, because it involves things like Pack (Unpack u) ~ u--- The type signature is intentionally left off here to check that the--- compiler can infer it.--- z :: forall a (u :: Unit) (v :: Unit). (Fractional a, Convertible u v)---   => Quantity a u---   -> Quantity a v-{-# ANN z "HLint: ignore Eta reduce" #-}-z q = convert q---- Pattern splices are supported, albeit with restricted types-patternSplice [u| 2 m |] [u| 0.0 kg / s |] = True-patternSplice [u| 1 m |] [u| 0.1 kg / s |] = True-patternSplice _          _                 = False---- Andrew's awkward generalisation example is accepted only with a--- type signature, even with NoMonoLocalBinds-tricky :: forall a u . Num a => Quantity a u -> (Quantity a (u *: Base "m"), Quantity a (u *: Base "kg"))-tricky x = let f :: Quantity a v -> Quantity a (u *: v)-               f = (x *:)-           in (f [u| 3 m |], f [u| 5 kg |])----- Test that basic constraints involving exponentiation work-pow :: Quantity a (u *: (v ^: i)) -> Quantity a ((v ^: i) *: u)-pow = id----- This declares a synonym for One-[u| dimensionless = 1 |]-dimensionless :: Quantity a [u|dimensionless|] -> Quantity a [u|1|]-dimensionless = id---- This declares a dimensionless unit that requires explicit conversion-[u| dime = 1 1 |]-dime :: Fractional a => Quantity a [u|dime|] -> Quantity a [u|1|]-dime = convert----- Runtime testsuite--main :: IO ()-main = defaultMain tests--tests :: TestTree-tests = testGroup "uom-plugin"-  [ testGroup "Showing constants"-    [ testCase "show 3m"                 $ show [u| 3 m |]                @?= "[u| 3 m |]"-    , testCase "show 3m/s"               $ show [u| 3 m/s |]              @?= "[u| 3 m / s |]"-    , testCase "show 3.2 s^2"            $ show [u| 3.2 s^2 |]            @?= "[u| 3.2 s^2 |]"-    , testCase "show 3.0 kg m^2 / m s^2" $ show [u| 3.0 kg m^2 / m s^2 |] @?= "[u| 3.0 kg m / s^2 |]"-    , testCase "show 1"                  $ show (mk 1)                    @?= "[u| 1 |]"-    , testCase "show 1 s^-1"             $ show [u| 1 s^-1 |]             @?= "[u| 1 s^-1 |]"-    , testCase "show 2 1 / kg s"         $ show [u| 2 1 / kg s |]         @?= "[u| 2 kg^-1 s^-1 |]"-    , testCase "show (1 % 2) kg"         $ show [u| 1 % 2 kg |]           @?= "[u| 0.5 kg |]"-    ]-  , testGroup "Basic operations"-    [ testCase "2 + 2"                   $ [u| 2 s |] +: [u| 2 s |]        @?= [u| 4 s |]-    , testCase "in m/s"                  $ inMetresPerSecond 5             @?= [u| 5 m/s |]-    , testCase "mean"                    $ mean [ [u| 2 N |], [u| 4 N |] ] @?= [u| 3 N |]-    , testCase "tricky generalisation"   $ tricky [u| 2 s |]               @?= ([u| 6 m s |], [u| 10 kg s |])-    , testCase "polymorphic zero"        $ [u| 0 |] @?= [u| 0 m |]-    , testCase "polymorphic frac zero"   $ [u| 0.0 |] @?= [u| 0.0 N / m |]-    ]-  , testGroup "Literal 1 (*:) Quantity _ u"-    [ testCase "_ = Double"-        $ 1 *: ([u| 1 m |] :: (Quantity Double (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Int"-        $ 1 *: ([u| 1 m |] :: (Quantity Int (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Integer"-        $ 1 *: ([u| 1 m |] :: (Quantity Integer (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Rational, 1 *: [u| 1 m |]"-        $ 1 *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Rational, mk (1 % 1) *: [u| 1 m |]"-        $ mk (1 % 1) *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Rational, 1 *: [u| 1 % 1 m |]"-        $ 1 *: ([u| 1 % 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Rational, mk (1 % 1) *: [u| 1 % 1 m |]"-        $ mk (1 % 1) *: ([u| 1 % 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]-    ]-  , testGroup "(1 :: Quantity _ One) (*:) Quantity _ u"-    [ testCase "_ = Double"-        $ (1 :: Quantity Double One) *: ([u| 1 m |] :: (Quantity Double (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Int"-        $ (1 :: Quantity Int One) *: ([u| 1 m |] :: (Quantity Int (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Integer"-        $ (1 :: Quantity Integer One) *: ([u| 1 m |] :: (Quantity Integer (Base "m"))) @?= [u| 1 m |]-    , testCase "_ = Int"-        $ (1 :: Quantity Rational One) *: ([u| 1 m |] :: (Quantity Rational (Base "m"))) @?= [u| 1 m |]-    ]-  , testGroup "errors when a /= b, (1 :: Quantity a One) (*:) Quantity b u"-    [ testGroup "b = Double"-      [ testCase "a = Int" $ op_a1 `throws` opErrors "Double" "Int" "Int"-      , testCase "a = Integer" $ op_a2 `throws` opErrors "Double" "Integer" "Integer"-      , testCase "a = Rational" $ op_a3 `throws` opErrors "Double" "GHC.Real.Ratio Integer" "Rational"-      ]-    , testGroup "b = Int"-      [ testCase "a = Double" $ op_b1 `throws` opErrors "Int" "Double" "Double"-      , testCase "a = Integer" $ op_b2 `throws` opErrors "Int" "Integer" "Integer"-      , testCase "a = Rational" $ op_b3 `throws` opErrors "Int" "GHC.Real.Ratio Integer" "Rational"-      ]-    , testGroup "b = Integer"-      [ testCase "a = Double" $ op_c1 `throws` opErrors "Integer" "Double" "Double"-      , testCase "a = Int" $ op_c2 `throws` opErrors "Integer" "Int" "Int"-      , testCase "a = Rational" $ op_c3 `throws` opErrors "Integer" "GHC.Real.Ratio Integer" "Rational"-      ]-    , testGroup "b = Rational"-      [ testCase "a = Double" $ op_d1 `throws` opErrors "GHC.Real.Ratio Integer" "Double" "Double"-      , testCase "a = Int" $ op_d2 `throws` opErrors "GHC.Real.Ratio Integer" "Int" "Int"-      , testCase "a = Integer" $ op_d3 `throws` opErrors "GHC.Real.Ratio Integer" "Integer" "Integer"-      ]-    ]-  , testGroup "showQuantity"-    [ testCase "myMass"         $ showQuantity myMass         @?= "65.0 kg"-    , testCase "gravityOnEarth" $ showQuantity gravityOnEarth @?= "9.808 m / s^2"-    , testCase "forceOnGround"  $ showQuantity forceOnGround  @?= "637.52 kg m / s^2"-    ]-  , testGroup "convert"-    [ testCase "10m in ft"     $ convert [u| 10m |]   @?= [u| 32.8 ft |]-    , testCase "5 km^2 in m^2" $ convert [u| 5km^2 |] @?= [u| 5000000 m m |]-    , testCase "ratio"         $ show (ratio [u| ft |] [u| m |]) @?= "[u| 3.28 ft / m |]"-    , testCase "100l in m^3"   $ convert [u| 100l |]   @?= [u| 0.1 m^3 |]-    , testCase "1l/m in m^2"   $ convert [u| 1l/m |]   @?= [u| 0.001 m^2 |]-    , testCase "1l/m in m^2"   $ convert [u| 1l/m |]   @?= [u| 0.001 m^2 |]-    , testCase "5l in ft^3"    $ convert [u| 5l   |]   @?= [u| 0.17643776 ft^3 |]-    , testCase "2000000l^2 in ft^3 m^3" $ convert [u| 2000000l^2 |] @?= [u| 70.575104 ft^3 m^3 |]-    , testCase "42 rad/s in s^-1" $ convert [u| 42 rad/s |] @?= [u| 42 s^-1 |]-    , testCase "2.4 l/h in m" $ convert [u| 2.4 l/ha |] @?= [u| 2.4e-7 m |]-    , testCase "1 m^4 in l m" $ convert [u| 1 m^4 |] @?= [u| 1000 l m |]-    ]-  , testGroup "errors"-    [ testCase "s/m ~ m/s"            $ mismatch1 `throws` mismatch1_errors-    , testCase "m + s"                $ mismatch2 `throws` mismatch2_errors-    , testCase "a ~ a  =>  a ~ kg"    $ given1 undefined `throws` given1_errors-    , testCase "a ~ b  =>  a ~ kg"    $ given2 undefined `throws` given2_errors-    , testCase "a^2 ~ b^3  =>  a ~ s" $ given3 undefined `throws` given3_errors-    ]-  , testGroup "read . show"-    [ testCase "3 m"     $ read (show [u| 3 m     |]) @?= [u| 3 m     |]-    , testCase "1.2 m/s" $ read (show [u| 1.2 m/s |]) @?= [u| 1.2 m/s |]-    , testCase "0"       $ read (show [u| 1       |]) @?= [u| 1       |]-    ]-  , testGroup "read normalisation"-    [ testCase "1 m/m"       $ read "[u| 1 m/m |]"       @?= [u| 1 |]-    , testCase "-0.3 m s^-1" $ read "[u| -0.3 m s^-1 |]" @?= [u| -0.3 m/s |]-    , testCase "42 s m s"    $ read "[u| 42 s m s |]"    @?= [u| 42 m s^2 |]-    ]-  ]----- | Assert that evaluation of the first argument (to WHNF) will throw--- an exception whose string representation contains one of the given--- lists of substrings.-throws :: a -> [[String]] -> Assertion-throws v xs =-    (evaluate v >> assertFailure "No exception!") `catch` \ (e :: SomeException) ->-        unless (any (all (`isInfixOf` show e)) xs) $ throw e

@@ -1,15 +1,10 @@--- This file has been generated from package.yaml by hpack version 0.28.2.------ see: https://github.com/sol/hpack------ hash: d110f2f74fb66155437b924f27283bd9b16991b4f2be45693731488d98f4938c+cabal-version: 1.12  name:           uom-plugin-version:        0.3.0.0-synopsis:       Units of measure as a GHC typechecker plugin-description:    The @uom-plugin@ library adds support for units of measure to GHC-                using the new experimental facility for typechecker plugins, which-                is available in GHC 7.10 and later.  See+version:        0.4.0.0+synopsis:       Units of measure as a GHC type-checker plugin+description:    The @uom-plugin@ library adds support for units of+                measure as a GHC type-checker plugin. See                 "Data.UnitsOfMeasure.Tutorial" for an introduction to the library. category:       Type System stability:      experimental@@ -17,16 +12,15 @@ bug-reports:    https://github.com/adamgundry/uom-plugin/issues author:         Adam Gundry <adam@well-typed.com> maintainer:     Adam Gundry <adam@well-typed.com>-copyright:      Copyright (c) 2014-2018, Adam Gundry+copyright:      Copyright (c) 2014-2022, Adam Gundry license:        BSD3 license-file:   LICENSE-tested-with:    GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2-+tested-with:    GHC == 9.0.2, GHC == 9.2.4, GHC == 9.4.2 build-type:     Simple-cabal-version:  >= 1.10 extra-source-files:-    changelog-    package.yaml+    CHANGELOG.md+    README.md+    LICENSE  source-repository head   type: git@@ -48,47 +42,83 @@       Data.UnitsOfMeasure.Plugin.NormalForm       Data.UnitsOfMeasure.Plugin.Unify       Data.UnitsOfMeasure.TH-      TcPluginExtras-      Paths_uom_plugin+      GhcApi+      GhcApi.Compare   hs-source-dirs:+      doc       src   ghc-options: -Wall -fno-warn-unticked-promoted-constructors   build-depends:-      base >=4.7 && <5-    , containers >=0.5 && <0.6+      base >=4.9.1.0 && <5+    , containers >=0.5 && <0.7     , deepseq >=1.3 && <1.5-    , ghc >=7.9 && <8.4-    , ghc-tcplugins-extra >=0.1 && <0.3-    , template-haskell >=2.9 && <2.13+    , ghc >=9.0.1 && <9.5+    , ghc-tcplugin-api >=0.8.3.0 && <0.9+    , template-haskell >=2.9 && <2.20     , units-parser >=0.1 && <0.2   default-language: Haskell2010 +test-suite doctest+  if impl(ghc >= 9.4)+      buildable: False+  type: exitcode-stdio-1.0+  main-is: DocTest.hs+  other-modules:+      Data.UnitsOfMeasure+      Data.UnitsOfMeasure.Convert+      Data.UnitsOfMeasure.Defs+      Data.UnitsOfMeasure.Internal+      Data.UnitsOfMeasure.Plugin+      Data.UnitsOfMeasure.Plugin.Convert+      Data.UnitsOfMeasure.Plugin.NormalForm+      Data.UnitsOfMeasure.Plugin.Unify+      Data.UnitsOfMeasure.Read+      Data.UnitsOfMeasure.Show+      Data.UnitsOfMeasure.Singleton+      Data.UnitsOfMeasure.TH+      GhcApi+      GhcApi.Compare+  hs-source-dirs:+      src+      test-suite-doctest+  ghc-options: -Wall -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N+  build-depends:+      QuickCheck+    , base >=4.9.1.0 && <5+    , containers >=0.5+    , deepseq >=1.3 && <1.5+    , doctest+    , ghc+    , ghc-tcplugin-api+    , template-haskell >=2.9+    , units-parser >=0.1+  default-language: Haskell2010+ test-suite hlint+  buildable: False   type: exitcode-stdio-1.0   main-is: HLint.hs-  other-modules:-      Paths_uom_plugin   hs-source-dirs:-      hlint-  ghc-options: -Wall -fno-warn-unticked-promoted-constructors -Wall -O0 -rtsopts -threaded -with-rtsopts=-N+      test-suite-hlint+  ghc-options: -Wall -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N   build-depends:-      base-    , hlint >=1.7 && <2.2+      base >=4.9.1.0 && <5+    , hlint >=2.0.11   default-language: Haskell2010  test-suite units   type: exitcode-stdio-1.0   main-is: Tests.hs   other-modules:+      Defs       ErrorTests-      Paths_uom_plugin+      Z   hs-source-dirs:-      tests-  other-extensions: TemplateHaskell-  ghc-options: -Wall -fno-warn-unticked-promoted-constructors -O0+      test-suite-units+  ghc-options: -Wall -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N   build-depends:-      base-    , tasty >=0.10 && <1.1-    , tasty-hunit >=0.9 && <0.10.1+      base >=4.9.1.0 && <5+    , tasty >=0.11.3+    , tasty-hunit >=0.9.2     , uom-plugin   default-language: Haskell2010