packages feed

uom-plugin (empty) → 0.1.0.0

raw patch · 18 files changed

+2056/−0 lines, 18 filesdep +basedep +containersdep +ghcsetup-changed

Dependencies added: base, containers, ghc, ghc-tcplugins-extra, tasty, tasty-hunit, template-haskell, units-parser, uom-plugin

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Adam Gundry++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Adam Gundry nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Data/UnitsOfMeasure.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- | See "Data.UnitsOfMeasure.Tutorial" for how to use this module.+module Data.UnitsOfMeasure+    ( -- * Type-level units of measure+      Unit+    , type Base+    , type One+    , type (*:)+    , type (/:)+    , type (^:)++      -- * Values indexed by their units+    , Quantity+    , unQuantity+    , zero+    , mk++      -- * Unit-safe 'Num' operations+    , (+:)+    , (*:)+    , (-:)+    , negate'+    , abs'+    , signum'+    , fromInteger'++      -- * Unit-safe 'Fractional' operations+    , (/:)+    , recip'+    , fromRational'++      -- * Unit-safe 'Floating' operations+    , sqrt'++      -- * TH constructor for quantities/units+    , u++      -- * Declaring units+    , declareBaseUnit+    , declareDerivedUnit+    , declareConvertibleUnit++      -- * Automatic unit conversions+    , convert++      -- * Pay no attention to that man behind the curtain+    , MkUnit+    , Pack+    , Unpack+    , KnownUnit+    ) where++import Data.UnitsOfMeasure.Convert+import Data.UnitsOfMeasure.Internal+import Data.UnitsOfMeasure.Show ()+import Data.UnitsOfMeasure.Singleton+import Data.UnitsOfMeasure.TH
+ src/Data/UnitsOfMeasure/Convert.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}++-- | Experimental support for conversions between units with the same+-- dimension, for example feet and metres.  This interface is not+-- necessarily stable!+--+-- Rather than defining dimensions explicitly, we pick a "canonical"+-- base unit for each dimension, and record the conversion ratio+-- between each base unit and the canonical base unit for its+-- dimension.  This means we can automatically calculate the+-- conversion ratio between a unit and its canonical representation,+-- and hence between any two units that share a dimension (i.e. have+-- the same canonical representation).+--+-- For example, to declare @m@ as a canonical base unit, write:+--+-- > instance HasCanonicalBaseUnit "m"+--+-- To declare @ft@ as a derived unit, write:+--+-- > instance HasCanonicalBaseUnit "ft" where+-- >   type CanonicalBaseUnit "ft" = "m"+-- >   conversionBase _ = [u| 3.28 ft/m |]+--+-- The above declarations can be written using the 'u' declaration+-- quasiquoter as @['u'| m, ft = 1 % 3.28 ft/m |]@, or generated+-- automatically using 'declareConvertibleUnit'.+--+-- Now it is possible to 'convert' between quantities whose units+-- involve feet or metres.  For example:+--+-- >>> convert [u| 10m |] :: Quantity Double [u| ft |]+-- [u| 32.8 ft |]+-- >>> convert [u| 3ft^2 |] :: Quantity Double [u| m^2 |]+-- [u| 0.27885187388459254 m^2 |]+--+-- You are likely to get unpleasant compiler error messages if you+-- attempt to convert without the units being fully determined by type+-- inference, or if the units do not have the same dimension.+module Data.UnitsOfMeasure.Convert+    ( convert+    , ratio+    , HasCanonicalBaseUnit(..)+      -- * Constraints+    , Good+    , HasCanonical+    , Convertible+    , ToCanonicalUnit+    , MapCBU+    ) where++import Data.UnitsOfMeasure.Internal+import Data.UnitsOfMeasure.Singleton++import GHC.Exts ( Constraint )+import GHC.TypeLits+++-- | Class to capture the dimensions to which base units belong.  For+-- a canonical base unit, the class instance can be left empty.+class (CanonicalBaseUnit (CanonicalBaseUnit b) ~ CanonicalBaseUnit b)+    => HasCanonicalBaseUnit (b :: Symbol) where+  -- | The canonical base unit for this base unit.  If @b@ is+  -- canonical, then @'CanonicalBaseUnit' b = b@.  Otherwise,+  -- @'CanonicalBaseUnit' b@ must itself be canonical.+  type CanonicalBaseUnit b :: Symbol+  type CanonicalBaseUnit b = b++  -- | The conversion ratio between this base unit and its canonical+  -- base unit.  If @b@ is canonical then this ratio is @1@.+  conversionBase :: proxy b -> Quantity Rational (Base b /: Base (CanonicalBaseUnit b))+  default conversionBase :: (b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: Base b)+  conversionBase _ = 1++-- | Convert a unit into its canonical representation, where units are+-- represented syntactically.+type family MapCBU (u :: UnitSyntax Symbol) :: UnitSyntax Symbol where+  MapCBU (xs :/ ys) = ListMapCBU xs :/ ListMapCBU ys++type family ListMapCBU (xs :: [Symbol]) :: [Symbol] where+  ListMapCBU '[]             = '[]+  ListMapCBU (x ': xs) = CanonicalBaseUnit x ': ListMapCBU 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+  HasCanonical (xs :/ ys) = (AllHasCanonical xs, AllHasCanonical ys)++type family AllHasCanonical (xs :: [Symbol]) :: Constraint where+  AllHasCanonical '[] = ()+  AllHasCanonical (x ': xs) = (HasCanonicalBaseUnit x, AllHasCanonical xs)+++conversionRatio :: forall proxy u . Good u+               => proxy u -> Quantity Rational (u /: Pack (MapCBU (Unpack u)))+conversionRatio _ = help (unitSing :: SUnit (Unpack u))++help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: Pack (MapCBU u))+help (SUnit xs ys) = help' xs /: help' ys++help' :: forall xs . AllHasCanonical xs => SList xs -> Quantity Rational (Prod xs /: Prod (ListMapCBU xs))+help' SNil         = 1+help' (SCons p xs) = conversionBase p *: help' xs+++-- | A unit is "good" if all its base units have been defined, and+-- have associated canonical base units.+type Good            u = (u ~ Pack (Unpack u), KnownUnit (Unpack u), HasCanonical (Unpack u))++-- | Two units are convertible if they are both 'Good' and they have+-- the same canonical units (and hence the same dimension).+type Convertible   u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v)++-- | Converts a unit to the corresponding canonical representation.+type ToCanonicalUnit u = Pack (MapCBU (Unpack u))++-- | Automatically convert a quantity with units @u@ so that its units+-- 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)) *:)++-- | 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' .+         (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)
+ src/Data/UnitsOfMeasure/Defs.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}++-- | This module exports some example definitions of base and derived+-- units, for demonstration purposes.  In the future, this is likely+-- to change or be moved to a separate package.+module Data.UnitsOfMeasure.Defs+    ( MkUnit+    ) where++import Data.UnitsOfMeasure++-- The SI base units+-- http://www.bipm.org/en/measurement-units/+[u| m, kg, s, A, K, mol, cd |]++-- Some prefixed units+[u| km = 1000m, g = 0.001 kg |]++-- SI derived units+-- http://physics.nist.gov/cuu/Units/units.html+[u| Hz = s^-1+  , N  = kg m / s^2+  , Pa = N / m^2+  , J  = N m+  , W  = J / s+  , C  = s A+  , V  = W / A+  , F  = C / V+  , ohm = V / A+ |]++-- Non-SI units accepted for use with them+-- http://www.bipm.org/en/publications/si-brochure/chapter4.html+[u| min = 60 s, h = 3600 s, d, ha, l, t, au |]++-- Some random other units+[u| ft = 100 % 328 m, in = 0.0254 m, mi = 1609.344 m, mph = mi/h |]
+ src/Data/UnitsOfMeasure/Internal.hs view
@@ -0,0 +1,248 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- | This module defines the core types used in the @uom-plugin@+-- library.  Note that importing this module may allow you to violate+-- invariants, so you should generally work with the safe interface in+-- "Data.UnitsOfMeasure" instead.+module Data.UnitsOfMeasure.Internal+    ( -- * Type-level units of measure+      Unit+    , type One+    , type Base+    , type (*:)+    , type (/:)+    , type (^:)++      -- * Values indexed by their units+    , Quantity(..)+    , unQuantity+    , zero+    , mk++      -- * Unit-safe 'Num' operations+    , (+:)+    , (*:)+    , (-:)+    , negate'+    , abs'+    , signum'+    , fromInteger'++      -- * Unit-safe 'Fractional' operations+    , (/:)+    , recip'+    , fromRational'++      -- * Unit-safe 'Floating' operations+    , sqrt'++      -- * Syntactic representation of units+    , UnitSyntax(..)+    , Unpack+    , Pack+    , Prod++      -- * Internal+    , type (~~)+    , MkUnit+    ) where++import GHC.Exts (Constraint)+import GHC.TypeLits (Symbol, Nat, type (-))++-- | (Kind) Units of measure+data Unit++-- | Dimensionless unit (identity element)+type family One :: Unit+#if __GLASGOW_HASKELL__ >= 711+  where+#endif++-- | Base unit+type family Base (b :: Symbol) :: Unit+#if __GLASGOW_HASKELL__ >= 711+  where+#endif++-- | Multiplication for units of measure+type family (u :: Unit) *: (v :: Unit) :: Unit+#if __GLASGOW_HASKELL__ >= 711+  where+#endif++-- | Division for units of measure+type family (u :: Unit) /: (v :: Unit) :: Unit+#if __GLASGOW_HASKELL__ >= 711+  where+#endif++-- | 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+  u ^: 0 = One+  u ^: 1 = u+  u ^: n = u *: (u ^: (n-1))++infixl 6 +:, -:+infixl 7 *:, /:+infixr 8 ^:++-- | A @Quantity a u@ is represented identically to a value of+-- underlying numeric type @a@, but with units @u@.+newtype Quantity a (u :: Unit) = MkQuantity a+  -- ^ Warning: the 'MkQuantity' constructor allows module invariants+  -- to be violated, so use it with caution!+type role Quantity representational nominal++-- These classes work uniformly on the underlying representation,+-- regardless of the units+deriving instance Bounded a => Bounded (Quantity a u)+deriving instance Eq      a => Eq      (Quantity a u)+deriving instance Ord     a => Ord     (Quantity a u)++-- These classes are not unit-polymorphic, so we have to restrict the+-- unit index to be dimensionless+deriving instance (Enum       a, u ~ One) => Enum       (Quantity a u)+deriving instance (Floating   a, u ~ One) => Floating   (Quantity a u)+deriving instance (Fractional a, u ~ One) => Fractional (Quantity a u)+deriving instance (Integral   a, u ~ One) => Integral   (Quantity a u)+deriving instance (Num        a, u ~ One) => Num        (Quantity a u)+deriving instance (Real       a, u ~ One) => Real       (Quantity a u)+deriving instance (RealFloat  a, u ~ One) => RealFloat  (Quantity a u)+deriving instance (RealFrac   a, u ~ One) => RealFrac   (Quantity a u)+++-- | Extract the underlying value of a quantity+unQuantity :: Quantity a u -> a+unQuantity (MkQuantity x) = x++-- | Zero is polymorphic in its units: this is required because the+-- 'Num' instance constrains the quantity to be dimensionless, so+-- @0 :: Quantity a u@ is not well typed.+zero :: Num a => Quantity a u+zero = MkQuantity 0++-- | Construct a 'Quantity' from a dimensionless value.  Note that for+-- numeric literals, the 'Num' and 'Fractional' instances allow them+-- to be treated as quantities directly.+mk :: a -> Quantity a One+mk = MkQuantity+++-- | 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)++-- | 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)++-- | 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)++-- | Negation ('negate') of quantities is polymorphic in the units.+negate' :: Num a => Quantity a u -> Quantity a u+negate' (MkQuantity x) = MkQuantity (negate x)++-- | 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)++-- | 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)++-- | Convert an 'Integer' quantity into any 'Integral' type ('fromInteger').+fromInteger' :: Integral a => Quantity Integer u -> Quantity a u+fromInteger' (MkQuantity x) = MkQuantity (fromInteger x)+++-- | 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)++-- | 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)++-- | Convert a 'Rational' quantity into any 'Fractional' type ('fromRational').+fromRational' :: Fractional a => Quantity Rational u -> Quantity a u+fromRational' (MkQuantity x) = MkQuantity (fromRational x)+++-- | 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)+++-- | Syntactic representation of a unit as a pair of lists of base+-- units, for example 'One' is represented as @[] ':/' []@ and+-- @'Base' "m" '/:' 'Base' "s" ^: 2@ is represented as @["m"] ':/' ["s","s"]@.+data UnitSyntax s = [s] :/ [s]++-- | Pack up a syntactic representation of a unit as a unit.  For example:+--+-- @ 'Pack' ([] ':/' []) = 'One' @+--+-- @ 'Pack' (["m"] ':/' ["s","s"]) = 'Base' "m" '/:' 'Base' "s" ^: 2 @+--+-- This is a perfectly ordinary closed type family.  'Pack' is a left+-- 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+  Pack (xs :/ ys) = Prod xs /: Prod ys++-- | Take the product of a list of base units.+type family Prod (xs :: [Symbol]) :: Unit where+  Prod '[]       = One+  Prod (x ': xs) = Base x *: Prod xs++-- | Unpack a unit as a syntactic representation, where the order of+-- units is deterministic.  For example:+--+-- @ 'Unpack' 'One' = [] ':/' [] @+--+-- @ 'Unpack' ('Base' "s" '*:' 'Base' "m") = ["m","s"] ':/' [] @+--+-- This does not break type soundness because+-- 'Unpack' will reduce only when the unit is entirely constant, and+-- 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+++-- | 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++infix 4 ~~+++-- | This type family is used for translating unit names (as+-- type-level strings) into units.  It will be 'Base' for base units+-- or expand the definition for derived units.+--+-- The instances displayed by Haddock are available only if+-- "Data.UnitsOfMeasure.Defs" is imported.+type family MkUnit (s :: Symbol) :: Unit
+ src/Data/UnitsOfMeasure/Plugin.hs view
@@ -0,0 +1,198 @@+{-# LANGUAGE CPP #-}++-- | This module defines a typechecker plugin that solves equations+-- involving units of measure.  To use it, add+--+-- > {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}+--+-- above the module header of your source files, or in the+-- @ghc-options@ field of your @.cabal@ file.  You do not need to+-- import this module.+module Data.UnitsOfMeasure.Plugin+  ( plugin+  ) where++import Plugins++import TcEvidence+import TcRnTypes+import TcType+import TcPluginM++import Coercion+import DataCon+import Type+import TyCon+import TypeRep+import TysWiredIn++import FastString+import Outputable++import OccName ( occName, occNameFS, mkTcOcc )+import Module++import Data.Either+import Data.List++import Data.UnitsOfMeasure.Plugin.Convert+import Data.UnitsOfMeasure.Plugin.NormalForm+import Data.UnitsOfMeasure.Plugin.Unify+import TcPluginExtras++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 }++uomPlugin :: TcPlugin+uomPlugin = tracePlugin "uom-plugin" $ TcPlugin { tcPluginInit  = lookupUnitDefs+                                               , tcPluginSolve = unitsOfMeasureSolver+                                               , 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+    case unit_givens of+      []    -> return $ TcPluginOk [] []+      (_:_) -> do+        sr <- simplifyUnits uds $ map snd unit_givens+        tcPluginTrace "unitsOfMeasureSolver simplified givens only" $ ppr sr+        return $ case sr of+          -- Simplified tvs []    evs eqs -> TcPluginOk (map (solvedGiven . fst) unit_givens) []+          Simplified _    -> TcPluginOk [] []+          Impossible eq _ -> TcPluginContradiction [fromUnitEquality 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)+++unitsOfMeasureSolver uds givens _deriveds wanteds = do+  xs <- lookForUnpacks uds givens wanteds+  case null xs of+   False -> return $ TcPluginOk [] xs+   True  -> do+    let (unit_wanteds, _) = partitionEithers $ map (toUnitEquality uds) wanteds+    case unit_wanteds of+      []    -> return $ TcPluginOk [] []+      (_:_) -> do+        (unit_givens , _) <- partitionEithers . map (toUnitEquality uds) <$> mapM zonkCt givens+        sr <- simplifyUnits uds unit_givens+        tcPluginTrace "unitsOfMeasureSolver simplified givens" $ ppr sr+        case sr of+          Impossible eq _ -> return $ TcPluginContradiction [fromUnitEquality eq]+          Simplified ss   -> do sr' <- simplifyUnits uds $ map (substsUnitEquality (simplifySubst ss)) unit_wanteds+                                tcPluginTrace "unitsOfMeasureSolver simplified wanteds" $ ppr sr'+                                case sr' of+                                  Impossible eq _ -> return $ TcPluginContradiction [fromUnitEquality $ substsUnitEquality (simplifyUnsubst ss) eq]+                                  Simplified ss'  -> TcPluginOk [ (evMagic uds ct, ct) | eq <- simplifySolved ss', let ct = fromUnitEquality eq ]+                                                         <$> mapM (substItemToCt uds) (filter (isWanted . ctEvidence . siCt) (substsSubst (simplifyUnsubst ss) (simplifySubst ss')))+++substItemToCt :: UnitDefs -> SubstItem -> TcPluginM Ct+substItemToCt uds si+      | isGiven (ctEvidence ct) = newGivenCt loc prd $ evByFiat "units" ty1 ty2+      | otherwise               = newWantedCt loc prd+      where+        prd  = mkEqPred 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 _  (TyVarTy _)      = []+    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 _  (LitTy _)        = []++    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++        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+++-- Extract the unit equality constraints+toUnitEquality :: UnitDefs -> Ct -> Either UnitEquality Ct+toUnitEquality uds ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+    EqPred NomEq t1 t2+      | isUnitKind uds (typeKind t1) || isUnitKind uds (typeKind t1)+      , Just u1 <- normaliseUnit uds t1+      , Just u2 <- normaliseUnit uds t2 -> Left (ct, u1, u2)+    IrredPred t+      | Just (tc, [t1,t2]) <- splitTyConApp_maybe t+      , tc == equivTyCon uds+      , Just u1 <- normaliseUnit uds t1+      , Just u2 <- normaliseUnit uds t2 -> Left (ct, u1, u2)+    _                                   -> Right ct++fromUnitEquality :: UnitEquality -> Ct+fromUnitEquality (ct, _, _) = ct+++lookupUnitDefs :: TcPluginM UnitDefs+lookupUnitDefs = do+    md <- lookupModule myModule myPackage+    u <- look md "Unit"+    b <- look md "Base"+    o <- look md "One"+    m <- look md "*:"+    d <- look md "/:"+    e <- look md "^:"+    x <- look md "Unpack"+    i <- look md "UnitSyntax"+    c <- look md "~~"+    return $ UnitDefs u b o m d e x i (getDataCon i ":/") c+  where+    getDataCon u s = case [ dc | dc <- tyConDataCons u, occNameFS (occName (dataConName dc)) == fsLit s ] of+                       [d] -> promoteDataCon d+                       _   -> error $ "lookupUnitDefs/getDataCon: missing " ++ s++    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)+    myModule  = mkModuleName "Data.UnitsOfMeasure.Internal"+    myPackage = fsLit "uom-plugin"+++-- | Produce bogus evidence for a constraint, including actual+-- equality constraints and our fake '(~~)' equality constraints.+evMagic :: UnitDefs -> Ct -> EvTerm+evMagic uds ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+    EqPred NomEq t1 t2   -> evByFiat "units" t1 t2+    IrredPred t+      | Just (tc, [t1,t2]) <- splitTyConApp_maybe t+      , tc == equivTyCon uds -> evByFiat "units" t1 t2 `EvCast`+                                  TcCoercion (mkUnivCo (fsLit "units") Representational (mkTyConApp eqTyCon [typeKind t1, t1, t2]) t)+    _                    -> error "evMagic"
+ src/Data/UnitsOfMeasure/Plugin/Convert.hs view
@@ -0,0 +1,79 @@+module Data.UnitsOfMeasure.Plugin.Convert+  ( UnitDefs(..)+  , unitKind+  , isUnitKind+  , normaliseUnit+  , reifyUnit+  ) where++import TyCon+import Type+import TypeRep+import TcType++import Data.List++import Data.UnitsOfMeasure.Plugin.NormalForm++-- | Contains references to the basic unit constructors declared in+-- "Data.UnitsOfMeasure", as loaded inside GHC.+data UnitDefs = UnitDefs+    { unitKindCon   :: TyCon -- ^ The 'Unit' type constructor, to be promoted to a kind+    , unitBaseTyCon :: TyCon -- ^ The 'Base' data constructor of 'Unit', promoted to a type constructor+    , unitOneTyCon  :: TyCon -- ^ The 'One'  type family+    , mulTyCon      :: TyCon -- ^ The '(*:)' type family+    , divTyCon      :: TyCon -- ^ The '(/:)' type family+    , expTyCon      :: TyCon -- ^ The '(^:)' type family+    , unpackTyCon     :: TyCon -- ^ The 'Unpack' type family+    , unitSyntaxTyCon :: TyCon -- ^ The 'UnitSyntax' type constructor, to be promoted to a kind+    , unitSyntaxPromotedDataCon :: TyCon -- ^ The data constructor of 'UnitSyntax', promoted to a type constructor+    , equivTyCon      :: TyCon -- ^ The '(~~)' type family+    }++-- | 'Unit' promoted to a kind+unitKind :: UnitDefs -> Kind+unitKind uds = TyConApp (promoteTyCon $ unitKindCon uds) []++-- | Is this the 'Unit' kind?+isUnitKind :: UnitDefs -> Kind -> Bool+isUnitKind uds ty | Just (tc, _) <- tcSplitTyConApp_maybe ty = tc == unitKindCon uds+                  | otherwise                                = False+++-- | Try to convert a type to a unit normal form; this does not check+-- the type has kind 'Unit', and may fail even if it does.+normaliseUnit :: UnitDefs -> Type -> Maybe NormUnit+normaliseUnit uds ty | Just ty1 <- tcView ty = normaliseUnit uds ty1+normaliseUnit _   (TyVarTy v)              = pure $ varUnit v+normaliseUnit uds (TyConApp tc tys)+  | tc == unitOneTyCon  uds                = pure one+  | tc == unitBaseTyCon uds, [x]    <- tys = pure $ baseUnit x+  | tc == mulTyCon      uds, [u, v] <- tys = (*:) <$> normaliseUnit uds u <*> normaliseUnit uds v+  | tc == divTyCon      uds, [u, v] <- tys = (/:) <$> normaliseUnit uds u <*> normaliseUnit uds v+  | tc == expTyCon      uds, [u, n] <- tys, Just i <- isNumLitTy n = (^:) <$> normaliseUnit uds u <*> pure i+  | isFamilyTyCon tc                       = pure $ famUnit tc tys+normaliseUnit _ _ = Nothing+++-- | Convert a unit normal form to a type expression of kind 'Unit'+reifyUnit :: UnitDefs -> NormUnit -> Type+reifyUnit uds u | null xs && null ys = oneTy+                | null ys            = foldr1 times xs+                | null xs            = oneTy `divide` foldr1 times ys+                | otherwise          = foldr1 times xs `divide` foldr1 times ys+  where+    (pos, neg) = partition ((> 0) . snd) $ ascending u+    xs = map fromAtom            pos+    ys = map (fromAtom . fmap negate) neg++    oneTy      = mkTyConApp (unitOneTyCon uds) []+    times  x y = mkTyConApp (mulTyCon uds) [x, y]+    divide x y = mkTyConApp (divTyCon uds) [x, y]++    fromAtom (a, n) = pow n (reifyAtom a)+    pow 1 ty = ty+    pow n ty = mkTyConApp (expTyCon uds) [ty, mkNumLitTy n]++    reifyAtom (BaseAtom s)    = mkTyConApp (unitBaseTyCon uds) [s]+    reifyAtom (VarAtom  v)    = mkTyVarTy  v+    reifyAtom (FamAtom f tys) = mkTyConApp f tys
+ src/Data/UnitsOfMeasure/Plugin/NormalForm.hs view
@@ -0,0 +1,191 @@+module Data.UnitsOfMeasure.Plugin.NormalForm+  ( Atom(..)+  , BaseUnit+  , NormUnit+    -- * Constructors+  , one+  , varUnit+  , baseUnit+  , famUnit+  , mkNormUnit++    -- * Algebraic operations+  , (*:)+  , (/:)+  , (^:)+  , invert++    -- * Predicates+  , isOne+  , isConstant+  , maybeConstant+  , isBase+  , divisible+  , occurs++    -- * Destructors+  , ascending+  , leftover+  , divideExponents+  , substUnit+  ) where++import Type+import TyCon+import VarSet++import FastString+import Outputable+import Util ( thenCmp )++import qualified Data.Foldable as Foldable+import qualified Data.Map as Map+import Data.List ( sortBy )+import Data.Maybe+import Data.Ord+++-- | Base units are just represented as strings, for simplicity+type BaseUnit = FastString++-- | An atom in the normal form is either a base unit, a variable or a+-- stuck type family application (but not one of the built-in type+-- families that correspond to group operations).+data Atom = BaseAtom Type | VarAtom TyVar | FamAtom TyCon [Type]++instance Eq Atom where+  a == b = compare a b == EQ++-- TODO: using cmpTypes here probably isn't ideal, but does it matter?+instance Ord Atom where+  compare (BaseAtom x)    (BaseAtom y)      = cmpType x y+  compare (BaseAtom _)    _                 = LT+  compare (VarAtom  _)    (BaseAtom _)      = GT+  compare (VarAtom  a)    (VarAtom  b)      = compare a b+  compare (VarAtom  _)    (FamAtom _ _)     = LT+  compare (FamAtom f tys) (FamAtom f' tys') = compare f f' `thenCmp` cmpTypes tys tys'+  compare (FamAtom _ _)   _                 = GT++instance Outputable Atom where+  ppr (BaseAtom b) = ppr b+  ppr (VarAtom  v) = ppr v+  ppr (FamAtom tc tys) = ppr tc <> text " " <> ppr tys+++-- | A unit normal form is a signed multiset of atoms; we maintain the+-- invariant that the map does not contain any zero values.+newtype NormUnit = NormUnit { _NormUnit :: Map.Map Atom Integer }++instance Outputable NormUnit where+    ppr = ppr . Map.map show . _NormUnit+++-- | The group identity, representing the dimensionless unit+one :: NormUnit+one = NormUnit Map.empty++-- | Construct a normalised unit from an atom+atom :: Atom -> NormUnit+atom a = NormUnit $ Map.singleton a 1++-- | Construct a normalised unit from a single variable+varUnit :: TyVar -> NormUnit+varUnit = atom . VarAtom++-- | Construct a normalised unit from a single base unit+baseUnit :: Type -> NormUnit+baseUnit = atom . BaseAtom++-- | Construct a normalised unit from a stuck type family application:+-- this must not be one of the built-in type families!+famUnit :: TyCon -> [Type] -> NormUnit+famUnit tc = atom . FamAtom tc++-- | Construct a normalised unit from a list of atom-exponent pairs+mkNormUnit :: [(Atom, Integer)] -> NormUnit+mkNormUnit = mkNormUnitMap . Map.fromList++-- | Construct a normalised unit from an atom-exponent map, applying+-- the signed multiset invariant+mkNormUnitMap :: Map.Map Atom Integer -> NormUnit+mkNormUnitMap =  NormUnit . Map.filter (/= 0)+++-- | Multiplication of normalised units+(*:) :: NormUnit -> NormUnit -> NormUnit+u *: v = mkNormUnitMap $ Map.unionWith (+) (_NormUnit u) (_NormUnit v)++-- | Division of normalised units+(/:) :: NormUnit -> NormUnit -> NormUnit+u /: v = u *: invert v++-- | Expontentiation of normalised units+(^:) :: NormUnit -> Integer -> NormUnit+_ ^: 0 = one+u ^: n = NormUnit $ Map.map (* n) $ _NormUnit u++infixl 7 *:, /:+infixr 8 ^:++-- | Invert a normalised unit+invert :: NormUnit -> NormUnit+invert = NormUnit . Map.map negate . _NormUnit+++-- | Test whether a unit is dimensionless+isOne :: NormUnit -> Bool+isOne = Map.null . _NormUnit++-- | Test whether a unit is constant (contains only base literals)+isConstant :: NormUnit -> Bool+isConstant = all isBaseLiteral . Map.keys . _NormUnit++-- | Extract the base units if a unit is constant+maybeConstant :: NormUnit -> Maybe [(BaseUnit, Integer)]+maybeConstant = mapM getBase . Map.toList . _NormUnit+  where+    getBase (BaseAtom ty, i) = (\ b -> (b, i)) <$> isStrLitTy ty+    getBase _                = Nothing++-- | Test whether an atom is a base unit (but not necessarily a+-- *literal*, e.g. it could be @Base b@ for some variable @b@)+isBase :: Atom -> Bool+isBase (BaseAtom _) = True+isBase _            = False++-- | Test whether an atom is a literal base unit+isBaseLiteral :: Atom -> Bool+isBaseLiteral (BaseAtom ty) = isJust $ isStrLitTy ty+isBaseLiteral _             = False++-- | Test whether all exponents in a unit are divisble by an integer+divisible :: Integer -> NormUnit -> Bool+divisible i = Foldable.all (\ j -> j `rem` i == 0) . _NormUnit++-- | Test whether a type variable occurs in a unit (possibly under a+-- type family application)+occurs :: TyVar -> NormUnit -> Bool+occurs a = any occursAtom . Map.keys . _NormUnit+  where+    occursAtom (BaseAtom ty)   = elemVarSet a $ tyVarsOfType ty+    occursAtom (VarAtom b)     = a == b+    occursAtom (FamAtom _ tys) = elemVarSet a $ tyVarsOfTypes 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++-- | Drop a variable from a unit+leftover :: TyVar -> NormUnit -> NormUnit+leftover a = NormUnit . Map.delete (VarAtom a) . _NormUnit++-- | Divide all the exponents in a unit by an integer+divideExponents :: Integer -> NormUnit -> NormUnit+divideExponents i = mkNormUnitMap . Map.map (`quot` i) . _NormUnit++-- | Substitute the first unit for the variable in the second unit+substUnit :: TyVar -> NormUnit -> NormUnit -> NormUnit+substUnit a v u = case Map.lookup (VarAtom a) $ _NormUnit u of+                    Nothing -> u+                    Just i  -> (v ^: i) *: leftover a u
+ src/Data/UnitsOfMeasure/Plugin/Unify.hs view
@@ -0,0 +1,182 @@+module Data.UnitsOfMeasure.Plugin.Unify+  ( SubstItem(..)+  , substsSubst+  , substsUnitEquality+  , UnitEquality+  , SimplifyState(..)+  , SimplifyResult(..)+  , simplifyUnits+  ) where++import FastString+import Name+import Outputable+import TcRnMonad ( Ct, isGiven, ctEvidence )+import TcType+import Type+import Var++import Data.UnitsOfMeasure.Plugin.Convert+import Data.UnitsOfMeasure.Plugin.NormalForm+import TcPluginExtras+import TcPluginM+++-- | A substitution is essentially a list of (variable, unit) pairs,+-- but we keep the original 'Ct' that lead to the substitution being+-- made, for use when turning the substitution back into constraints.+type TySubst = [SubstItem]++data SubstItem = SubstItem { siVar     :: TyVar+                           , siUnit    :: NormUnit+                           , siCt     ::  Ct+                           }++instance Outputable SubstItem where+  ppr si = ppr (siVar si) <+> text " := " <+> ppr (siUnit si) <+> text "  {" <+> ppr (siCt si) <+> text "}"++-- | Apply a substitution to a single normalised unit+substsUnit :: TySubst -> NormUnit -> NormUnit+substsUnit []     u = u+substsUnit (si:s) u = substsUnit s (substUnit (siVar si) (siUnit si) u)++-- | Compose two substitutions+substsSubst :: TySubst -> TySubst -> TySubst+substsSubst s = map $ \ si -> si { siUnit = substsUnit s (siUnit si) }++substsUnitEquality :: TySubst -> UnitEquality -> UnitEquality+substsUnitEquality s (ct, u, v) = (ct, substsUnit s u, substsUnit s v)++extendSubst :: SubstItem -> TySubst -> TySubst+extendSubst si s = si : substsSubst [si] s+++-- | Possible results of unifying a single pair of units.  In the+-- non-failing cases, we return a substitution and a list of fresh+-- variables that were created.+data UnifyResult = Win [TyVar] TySubst TySubst+                 | Draw [TyVar] TySubst TySubst+                 | Lose++instance Outputable UnifyResult where+  ppr (Win  tvs subst unsubst) = text "Win"  <+> ppr tvs <+> ppr subst <+> ppr unsubst+  ppr (Draw tvs subst unsubst) = text "Draw" <+> ppr tvs <+> ppr subst <+> ppr unsubst+  ppr Lose                     = text "Lose"+++-- | 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 (ct, u0, v0) = do tcPluginTrace "unifyUnits" (ppr u0 $$ ppr v0)+                                 unifyOne uds ct [] [] [] (u0 /: v0)++unifyOne :: UnitDefs -> Ct -> [TyVar] -> TySubst -> TySubst -> NormUnit -> TcPluginM 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)++      where+        go :: [(Atom, Integer)] -> [(Atom, Integer)] -> TcPluginM 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+            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+                                                              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+            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+++        given_mode = isGiven (ctEvidence ct)++        newUnitVar | given_mode = newSkolemTyVar $ unitKind uds+                   | otherwise  = newFlexiTyVar  $ unitKind uds++        newSkolemTyVar kind = do+            x <- newUnique+            let name = mkSysTvName x (fsLit "beta")+            return $ mkTcTyVar name kind vanillaSkolemTv+++type UnitEquality = (Ct, NormUnit, NormUnit)++data SimplifyState+  = SimplifyState { simplifyFreshVars :: [TyVar]+                  , simplifySubst     :: TySubst+                  , simplifyUnsubst   :: TySubst+                  , simplifySolved    :: [UnitEquality]+                  , simplifyStuck     :: [UnitEquality]+                  }++instance Outputable SimplifyState where+  ppr ss = text "fresh   = " <+> ppr (simplifyFreshVars ss)+        $$ text "subst   = " <+> ppr (simplifySubst     ss)+        $$ text "unsubst = " <+> ppr (simplifyUnsubst   ss)+        $$ text "solved  = " <+> ppr (simplifySolved    ss)+        $$ text "stuck   = " <+> ppr (simplifyStuck     ss)++initialState :: SimplifyState+initialState = SimplifyState [] [] [] [] []++data SimplifyResult+  = Simplified SimplifyState+  | Impossible { simplifyImpossible :: UnitEquality+               , simplifyRemaining  :: [UnitEquality]+               }++instance Outputable SimplifyResult where+  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+  where+    simples :: SimplifyState -> [UnitEquality] -> TcPluginM SimplifyResult+    simples ss [] = return $ Simplified ss+    simples ss (eq:eqs) = do+        ur <- unifyUnits uds (substsUnitEquality (simplifySubst ss) eq)+        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)+          Draw _   []    _       -> simples (addStuck eq ss) eqs+          Draw tvs subst unsubst -> let (ss', xs) = draw eq tvs subst unsubst ss+                                    in simples ss' (xs ++ eqs)+          Lose                   -> return Impossible { simplifyImpossible = eq+                                                      , simplifyRemaining  = simplifyStuck ss ++ eqs }++win :: UnitEquality -> [TyVar] -> TySubst -> TySubst -> SimplifyState -> (SimplifyState, [UnitEquality])+win eq tvs subst unsubst ss =+  ( SimplifyState { simplifyFreshVars = simplifyFreshVars ss ++ tvs+                  , simplifySubst     = substsSubst subst (simplifySubst ss) ++ subst+                  , simplifyUnsubst   = substsSubst unsubst (simplifyUnsubst ss) ++ unsubst+                  , simplifySolved    = eq : simplifySolved ss+                  , simplifyStuck     = []+                  }+  , simplifyStuck ss )++draw :: UnitEquality -> [TyVar] -> TySubst -> TySubst -> SimplifyState -> (SimplifyState, [UnitEquality])+draw eq tvs subst unsubst ss =+  ( SimplifyState { simplifyFreshVars = simplifyFreshVars ss ++ tvs+                  , simplifySubst     = substsSubst subst (simplifySubst ss) ++ subst+                  , simplifyUnsubst   = substsSubst unsubst (simplifyUnsubst ss) ++ unsubst+                  , simplifySolved    = simplifySolved ss+                  , simplifyStuck     = [eq]+                  }+  , simplifyStuck ss )++addStuck :: UnitEquality -> SimplifyState -> SimplifyState+addStuck eq ss = ss { simplifyStuck = eq : simplifyStuck ss }
+ src/Data/UnitsOfMeasure/Show.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | Experimental support for showing units of measure in a pretty+-- syntax.  This requires the units to be fully determined.+--+-- Apart from the definitions below, this module also exports a 'Show'+-- instance for @'Quantity' a u@, which is re-exported by+-- "Data.UnitsOfMeasure".+module Data.UnitsOfMeasure.Show+    ( showQuantity+    , showUnit+    ) where++import Data.UnitsOfMeasure.Internal+import Data.UnitsOfMeasure.Singleton++import Data.List (intercalate, group)++instance (Show a, KnownUnit (Unpack u)) => Show (Quantity a u) where+  show x = "[u| " ++ showQuantity x ++ " |]"++-- | Render a quantity nicely, followed by its units:+--+-- >>> showQuantity (1 /: [u| 0.1 s / m kg |])+-- "10.0 kg m / s"+showQuantity :: forall a u. (Show a, KnownUnit (Unpack u)) => Quantity a u -> String+showQuantity (MkQuantity x) = show x ++ if s == "1" then "" else ' ':s+  where s = showUnit (undefined :: proxy u)++-- | Render a unit nicely:+--+-- >>> showUnit (undefined :: proxy [u| 1 / s |])+-- "s^-1"+showUnit :: forall proxy u . KnownUnit (Unpack u) => proxy u -> String+showUnit _ = showUnitBits (unitVal (undefined :: proxy' (Unpack u)))++showUnitBits :: UnitSyntax String -> String+showUnitBits ([] :/ []) = "1"+showUnitBits (xs :/ []) = showPos xs+showUnitBits ([] :/ ys) = showNeg ys+showUnitBits (xs :/ ys) = showPos xs ++ " / " ++ showPos ys++showPos :: [String] -> String+showPos = intercalate " " . map (\ xs -> showAtom (head xs, length xs)) . group++showNeg :: [String] -> String+showNeg = intercalate " " . map (\ xs -> showAtom (head xs, negate $ length xs)) . group++showAtom :: (String, Int) -> String+showAtom (s, 1) = s+showAtom (s, i) = s ++ "^" ++ show i
+ src/Data/UnitsOfMeasure/Singleton.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++-- | This module defines singleton types for integers and concrete+-- units.+module Data.UnitsOfMeasure.Singleton+    ( -- * Singletons for units+      SUnit(..)+    , forgetSUnit+    , KnownUnit(..)+    , unitVal++      -- * Singletons for lists+    , SList(..)+    , KnownList(..)+    ) where++import GHC.TypeLits++import Data.UnitsOfMeasure.Internal+++-- | Singleton type for concrete units of measure represented as lists+-- of base units+data SUnit (u :: UnitSyntax Symbol) where+  SUnit :: SList xs -> SList ys -> SUnit (xs :/ ys)++-- | Singleton type for lists of base units+data SList (xs :: [Symbol]) where+  SNil :: SList '[]+  SCons :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs)++-- | Extract the runtime syntactic representation from a singleton unit+forgetSUnit :: SUnit u -> UnitSyntax String+forgetSUnit (SUnit xs ys) = forgetSList xs :/ forgetSList ys++forgetSList :: SList xs -> [String]+forgetSList SNil = []+forgetSList (SCons px xs) = symbolVal px : forgetSList xs+++-- | A constraint @'KnownUnit' u@ means that @u@ must be a concrete+-- unit that is statically known but passed at runtime+class KnownUnit (u :: UnitSyntax Symbol) where+  unitSing :: SUnit u++instance (KnownList xs, KnownList ys) => KnownUnit (xs :/ ys) where+  unitSing = SUnit listSing listSing+++-- | A constraint @'KnownList' xs@ means that @xs@ must be a list of+-- base units that is statically known but passed at runtime+class KnownList (xs :: [Symbol]) where+  listSing :: SList xs++instance KnownList '[] where+  listSing = SNil++instance (KnownSymbol x, KnownList xs) => KnownList (x ': xs) where+  listSing = SCons (undefined :: proxy x) listSing+++-- | Extract the runtime syntactic representation of a 'KnownUnit'+unitVal :: forall proxy u . KnownUnit u => proxy u -> UnitSyntax String+unitVal _ = forgetSUnit (unitSing :: SUnit u)
+ src/Data/UnitsOfMeasure/TH.hs view
@@ -0,0 +1,206 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}++-- | Template Haskell utilities for working with units of measure in a+-- nice syntax.+module Data.UnitsOfMeasure.TH+    ( u+    , declareBaseUnit+    , declareDerivedUnit+    , declareConvertibleUnit+    ) where++import Data.Char+import Numeric+import Text.Parse.Units++import Language.Haskell.TH+import Language.Haskell.TH.Quote++import Data.UnitsOfMeasure.Internal+import Data.UnitsOfMeasure.Convert++-- | The 'u' quasiquoter may be used to create units or quantities;+-- its meaning depends on the context:+--+-- * in a declaration context, it creates new base and derived units+--   from a comma-separated list of names with optional definitions,+--   for example @['u'|kg, m, s, N = kg * m/s^2|]@;+--+-- * in a type context, it parses a single unit and converts it into+--   the corresponding type, so @['u'|m/s|]@ becomes the type+--   @'Base' "m" /: 'Base' "s"@ of kind 'Unit';+--+-- * in an expression context, it can be used to create a 'Quantity'+--   corresponding to a numeric literal, for example @['u'|42 m|]@ is+--   an expression of type @'Quantity' 'Integer' ('Base' "m")@,+--   @['u'|-2.2 m|]@ is an expression of type @'Quantity' 'Double' ('Base' "m")@,+--   and @['u'|m|]@ alone is a function of type @a -> 'Quantity' a ('Base' "m")@;+--+-- * in a pattern context, it can be used to match on a particular+--   value of a quantity with an 'Integer' or 'Rational'+--   representation type, for example @f ['u'| 42 m |] = 'True'@ is a+--   (partial) function of type @'Quantity' 'Integer' [u|m|] -> Bool@.+--+u :: QuasiQuoter+u = QuasiQuoter+      { quoteExp  = uExp+      , quotePat  = uPat+      , quoteType = uType+      , quoteDec  = uDec+      }++-- | Parse a unit expression optionally preceded by a literal, and+-- create a constructor for 'Quantity' with the given units (applied+-- to the literal if one is present).+uExp :: String -> Q Exp+uExp s+  | Just (ei, s') <- readNumber s = mkLiteral ei =<< parseUnitQ s'+  | otherwise                     = mkConversion =<< parseUnitQ s+  where+    mkLiteral (Left  0) Unity = [| zero |]+    mkLiteral (Right 0) Unity = [| MkQuantity 0.0 |]+    mkLiteral ei        expr  = [| (MkQuantity :: a -> Quantity a $(reifyUnit expr))+                                                                  $(litE (either integerL rationalL ei)) |]+    mkConversion expr = [|  MkQuantity :: a -> Quantity a $(reifyUnit expr) |]++-- | Parse an integer or rational literal followed by a unit+-- expression, and create a pattern match on @'Quantity' 'Integer' u@+-- or @'Quantity' 'Rational' u@.  Unfortunately we cannot easily+-- support arbitrary representation types.+uPat :: String -> Q Pat+uPat s+  | Just (Left  i, s') <- readNumber s  = mkPat (integerL  i) [t|Integer |] s'+  | Just (Right r, s') <- readNumber s  = mkPat (rationalL r) [t|Rational|] s'+  | otherwise                           = error "unable to parse literal"+  where+    mkPat l t s' = [p| MkQuantity $(litP l) |] `sigP` [t| Quantity $t $(uType s') |]++-- | Parse a unit expression and convert it into the corresponding type.+uType :: String -> Q Type+uType s = reifyUnit =<< parseUnitQ s++parseUnitQ :: String -> Q (UnitExp () String)+parseUnitQ s = case parseUnit universalSymbolTable s of+                 Right expr -> return expr+                 Left  err  -> fail ("unable to parse unit expression \"" ++ s ++ "\": " ++ err)++-- | Convert a unit expression into the corresponding type.+reifyUnit :: UnitExp () String -> Q Type+reifyUnit Unity        = [t| One |]+reifyUnit (Unit _ s)   = [t| MkUnit $(litT (strTyLit s))            |]+reifyUnit (u `Mult` v) = [t| $(reifyUnit u) *: $(reifyUnit v)       |]+reifyUnit (u `Div`  v) = [t| $(reifyUnit u) /: $(reifyUnit v)       |]+reifyUnit (u `Pow`  n) | n >= 0    = [t| $(reifyUnit u) ^: $(litT (numTyLit n)) |]+                       | otherwise = [t| One /: $(reifyUnit u) ^: $(litT (numTyLit (- n))) |]+++-- | Parse the string as a mixture of base units and derived units,+-- and create corresponding 'MkUnit' type instance declarations.+uDec :: String -> Q [Dec]+uDec s = case parseUnitDecs s of+           Just xs -> concat <$> mapM (uncurry declareUnit) xs+           Nothing -> reportError ("unable to parse unit declarations: " ++ s) >> return []++data UnitDecl = BaseUnit+              | DefinedUnit    (UnitExp () String)+              | ConversionUnit Rational String++-- | Parse a comma-separated list of unit declarations, for example:+--+-- > kg, m, s, N = kg * m/s^2+parseUnitDecs :: String -> Maybe [(String, UnitDecl)]+parseUnitDecs = go+  where+    go [] = Just []+    go (c:xs) | isSpace c || c == ',' = go xs+    go xs = case span isAlpha xs of+              ([], _) -> Nothing+              (u, ys) -> go' u ys++    go' u [] = Just [(u, BaseUnit)]+    go' u (c:xs) | isSpace c = go' u xs+    go' u (',':xs) = ((u, BaseUnit) :) <$> go xs+    go' u ('=':xs) = let (d, ys) = break (== ',') xs+                     in case readNumber d of+                          Just (ei, s) -> case parseUnit universalSymbolTable s of+                                        Right (Unit _ e :: UnitExp () String) -> ((u, ConversionUnit (either fromInteger id ei) e) :) <$> go ys+                                        _                -> Nothing+                          _        -> case parseUnit universalSymbolTable d of+                                        Right e -> ((u, DefinedUnit e) :) <$> go ys+                                        Left  _ -> Nothing+    go' _ _        = Nothing++-- | Given a unit name and an optional definition, create an+-- appropriate instance of the 'MkUnit' type family.+declareUnit :: String -> UnitDecl -> Q [Dec]+declareUnit s ud = case ud of+  BaseUnit           -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s))+                            instance HasCanonicalBaseUnit $(litT (strTyLit s))+                          |]+  DefinedUnit u      -> [d| type instance MkUnit $(litT (strTyLit s)) = $(reifyUnit u) |]+  ConversionUnit r t -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s))+                            instance HasCanonicalBaseUnit $(litT (strTyLit s)) where+                              type CanonicalBaseUnit $(litT (strTyLit s)) = $(litT (strTyLit t))+                              conversionBase _ = MkQuantity $(litE (rationalL (recip r)))+                          |]++-- | Declare a canonical base unit of the given name, which must not+-- contain any spaces, e.g.+--+-- > declareBaseUnit "m"+--+-- produces+--+-- > type instance MkUnit "m" = Base "m"+-- > instance HasCanonicalBaseUnit "m"+--+-- This can also be written @['u'| m |]@.+declareBaseUnit :: String -> Q [Dec]+declareBaseUnit s = declareUnit s BaseUnit+++-- | Declare a derived unit with the given name and definition, e.g.+--+-- > declareDerivedUnit "N" "kg m / s^2"+--+-- produces+--+-- > type instance MkUnit "N" = Base "kg" *: Base "m" /: Base "s" ^: 2+--+-- This can also be written @['u'| N = kg m / s^2 |]@.+declareDerivedUnit :: String -> String -> Q [Dec]+declareDerivedUnit s d = case parseUnit universalSymbolTable d of+                           Right e -> declareUnit s (DefinedUnit e)+                           Left _  -> reportError ("unable to parse derived unit: " ++ d) >> return []++-- | Declare a base unit of the given name, which is convertible to+-- the canonical base unit, e.g.+--+-- > declareConvertibleUnit "kilobyte" 1024 "byte"+--+-- produces+--+-- > type instance MkUnit "kilobyte" = Base "kilobyte"+-- > instance HasCanonicalBaseUnit "kilobyte" where+-- >   type CanonicalBaseUnit "kilobyte" = "byte"+-- >   conversionBase _ = [u| 1 % 1024 kilobyte/byte |]+--+-- This can also be written @['u'| kilobyte = 1024 byte |]@.+-- See "Data.UnitsOfMeasure.Convert" for more information about conversions.+declareConvertibleUnit :: String -> Rational -> String -> Q [Dec]+declareConvertibleUnit derived r base = declareUnit derived (ConversionUnit r base)+++-- | Read either an integer or a rational from a string, if possible,+-- and return the remainder of the string.+readNumber :: String -> Maybe (Either Integer Rational, String)+readNumber s+  | [(r, s')] <- reads s                = Just (Right r, s')+  | [(i, s')] <- reads s                = Just (Left i , s')+  | [(r, s')] <- readSigned readFloat s = Just (Right r, s')+  | otherwise                           = Nothing
+ src/Data/UnitsOfMeasure/Tutorial.hs view
@@ -0,0 +1,171 @@+-- | 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>
+ src/TcPluginExtras.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RecordWildCards #-}++module TcPluginExtras+  ( -- * Wrappers+    newUnique+  , newWantedCt+  , newGivenCt+  ) where++import TcPluginM  ( TcPluginM )+import TcEvidence ( EvTerm )+import TcRnTypes  ( mkNonCanonical )+import TcRnMonad  ( Ct, CtLoc )+import Type       ( PredType )++import GHC.TcPluginM.Extra++#if __GLASGOW_HASKELL__ < 711+import Unique     ( Unique )+import qualified TcRnMonad+import TcPluginM ( unsafeTcPluginTcM )+#else+import TcPluginM ( newUnique )+#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 = fmap mkNonCanonical $ newGiven loc prd ev
+ tests/ErrorTests.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}++{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}+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)" ]+                ]+++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)" ]+                ]+++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)" ]+                ]
+ tests/Tests.hs view
@@ -0,0 +1,184 @@+{-# 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.Defs ()+import Data.UnitsOfMeasure.Show++import Control.Exception+import Data.List++import Test.Tasty+import Test.Tasty.HUnit++import ErrorTests+++-- Declarations+declareBaseUnit "byte"+declareDerivedUnit "bps" "byte / s"+declareConvertibleUnit "kilobyte" 1024 "byte"+++-- 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' xs = foldr (+:) zero xs+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+++-- 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+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+++-- 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 "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 |]"+    ]+  , 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+    ]+  ]+++-- | 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) -> if any (all (`isInfixOf` show e)) xs then return () else throw e
+ uom-plugin.cabal view
@@ -0,0 +1,61 @@+name:                uom-plugin+version:             0.1.0.0+synopsis:            Units of measure as a GHC typechecker plugin+category:            Type System+description:         A prototype typechecker plugin for GHC with support for units of measure+license:             BSD3+license-file:        LICENSE+author:              Adam Gundry <adam@well-typed.com>+maintainer:          Adam Gundry <adam@well-typed.com>+homepage:            https://github.com/adamgundry/uom-plugin+bug-reports:         https://github.com/adamgundry/uom-plugin/issues+stability:           experimental+copyright:           Copyright (c) 2014-2015, Adam Gundry+build-type:          Simple+cabal-version:       >=1.10+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.++source-repository head+  type:     git+  location: https://github.com/adamgundry/uom-plugin.git++library+  exposed-modules:     Data.UnitsOfMeasure,+                       Data.UnitsOfMeasure.Convert,+                       Data.UnitsOfMeasure.Defs,+                       Data.UnitsOfMeasure.Internal,+                       Data.UnitsOfMeasure.Plugin,+                       Data.UnitsOfMeasure.Show,+                       Data.UnitsOfMeasure.Singleton,+                       Data.UnitsOfMeasure.Tutorial+  other-modules:       Data.UnitsOfMeasure.Plugin.Convert,+                       Data.UnitsOfMeasure.Plugin.NormalForm,+                       Data.UnitsOfMeasure.Plugin.Unify,+                       Data.UnitsOfMeasure.TH,+                       TcPluginExtras+  other-extensions:    TemplateHaskell+  build-depends:       base >=4.7 && <5,+                       ghc >= 7.9 && <7.12,+                       ghc-tcplugins-extra >=0.1 && <0.2,+                       template-haskell >=2.9 && <2.12,+                       containers >=0.5 && <0.6,+                       units-parser >=0.1 && <0.2+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall -fno-warn-unticked-promoted-constructors++test-suite test-uom-plugin+  type:                exitcode-stdio-1.0+  main-is:             Tests.hs+  other-modules:       ErrorTests+  other-extensions:    TemplateHaskell+  build-depends:       base, uom-plugin,+                       tasty >=0.10 && <0.11, tasty-hunit >=0.9 && <0.10+  hs-source-dirs:      tests+  default-language:    Haskell2010+  ghc-options:         -O0