Guide type inference for Record type class instances via newtypes, not Proxies

src/Data/Bounded.purs

@@ -3,6 +3,7 @@ module Data.Bounded
   , bottom
   , top
   , module Data.Ord
+  , BRecord
   , class BoundedRecord
   , bottomRecord
   , topRecord
@@ -67,14 +68,20 @@ instance boundedProxy :: Bounded (Proxy a) where
   bottom = Proxy
   top = Proxy
 
+newtype BRecord :: RL.RowList Type -> Row Type -> Row Type -> Type
+newtype BRecord rowlist row subrow = BRecord { | subrow }
+
+unBRecord :: forall rowlist row subrow. BRecord rowlist row subrow -> { | subrow }
+unBRecord (BRecord r) = r
+
 class BoundedRecord :: RL.RowList Type -> Row Type -> Row Type -> Constraint
 class OrdRecord rowlist row <= BoundedRecord rowlist row subrow | rowlist -> subrow where
-  topRecord :: Proxy rowlist -> Proxy row -> Record subrow
-  bottomRecord :: Proxy rowlist -> Proxy row -> Record subrow
+  topRecord :: BRecord rowlist row subrow
+  bottomRecord :: BRecord rowlist row subrow
 
 instance boundedRecordNil :: BoundedRecord RL.Nil row () where
-  topRecord _ _ = {}
-  bottomRecord _ _ = {}
+  topRecord = BRecord {}
+  bottomRecord = BRecord {}
 
 instance boundedRecordCons ::
   ( IsSymbol key
@@ -84,22 +91,22 @@ instance boundedRecordCons ::
   , BoundedRecord rowlistTail row subrowTail
   ) =>
   BoundedRecord (RL.Cons key focus rowlistTail) row subrow where
-  topRecord _ rowProxy = insert top tail
+  topRecord = BRecord (insert top tail)
     where
     key = reflectSymbol (Proxy :: Proxy key)
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = topRecord (Proxy :: Proxy rowlistTail) rowProxy
+    tail = unBRecord (topRecord :: BRecord rowlistTail row subrowTail)
 
-  bottomRecord _ rowProxy = insert bottom tail
+  bottomRecord = BRecord (insert bottom tail)
     where
     key = reflectSymbol (Proxy :: Proxy key)
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = bottomRecord (Proxy :: Proxy rowlistTail) rowProxy
+    tail = unBRecord (bottomRecord :: BRecord rowlistTail row subrowTail)
 
 instance boundedRecord ::
   ( RL.RowToList row list
   , BoundedRecord list row row
   ) =>
   Bounded (Record row) where
-  top = topRecord (Proxy :: Proxy list) (Proxy :: Proxy row)
-  bottom = bottomRecord (Proxy :: Proxy list) (Proxy :: Proxy row)
+  top = unBRecord (topRecord :: BRecord list row row)
+  bottom = unBRecord (bottomRecord :: BRecord list row row)

src/Data/Eq.purs

@@ -7,6 +7,7 @@ module Data.Eq
   , class Eq1
   , eq1
   , notEq1
+  , ERecord
   , class EqRecord
   , eqRecord
   ) where
@@ -69,7 +70,7 @@ instance eqArray :: Eq a => Eq (Array a) where
   eq = eqArrayImpl eq
 
 instance eqRec :: (RL.RowToList row list, EqRecord list row) => Eq (Record row) where
-  eq = eqRecord (Proxy :: Proxy list)
+  eq l = eqRecord (ERecord l :: ERecord list row)
 
 instance eqProxy :: Eq (Proxy a) where
   eq _ _ = true
@@ -92,14 +93,17 @@ instance eq1Array :: Eq1 Array where
 notEq1 :: forall f a. Eq1 f => Eq a => f a -> f a -> Boolean
 notEq1 x y = (x `eq1` y) == false
 
+newtype ERecord :: RL.RowList Type -> Row Type -> Type
+newtype ERecord rowlist row = ERecord { | row }
+
 -- | A class for records where all fields have `Eq` instances, used to implement
 -- | the `Eq` instance for records.
 class EqRecord :: RL.RowList Type -> Row Type -> Constraint
 class EqRecord rowlist row where
-  eqRecord :: Proxy rowlist -> Record row -> Record row -> Boolean
+  eqRecord :: ERecord rowlist row -> Record row -> Boolean
 
 instance eqRowNil :: EqRecord RL.Nil row where
-  eqRecord _ _ _ = true
+  eqRecord _ _ = true
 
 instance eqRowCons ::
   ( EqRecord rowlistTail row
@@ -108,8 +112,8 @@ instance eqRowCons ::
   , Eq focus
   ) =>
   EqRecord (RL.Cons key focus rowlistTail) row where
-  eqRecord _ ra rb = (get ra == get rb) && tail
+  eqRecord (ERecord ra) rb = (get ra == get rb) && tail
     where
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
-    tail = eqRecord (Proxy :: Proxy rowlistTail) ra rb
+    tail = eqRecord (ERecord ra :: ERecord rowlistTail row) rb

src/Data/HeytingAlgebra.purs

@@ -8,6 +8,8 @@ module Data.HeytingAlgebra
   , not
   , (&&)
   , (||)
+  , H1Record
+  , H2Record
   , class HeytingAlgebraRecord
   , ffRecord
   , ttRecord
@@ -93,35 +95,44 @@ instance heytingAlgebraProxy :: HeytingAlgebra (Proxy a) where
   tt = Proxy
 
 instance heytingAlgebraRecord :: (RL.RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra (Record row) where
-  ff = ffRecord (Proxy :: Proxy list) (Proxy :: Proxy row)
-  tt = ttRecord (Proxy :: Proxy list) (Proxy :: Proxy row)
-  conj = conjRecord (Proxy :: Proxy list)
-  disj = disjRecord (Proxy :: Proxy list)
-  implies = impliesRecord (Proxy :: Proxy list)
-  not = notRecord (Proxy :: Proxy list)
+  ff = unH1Record (ffRecord :: H1Record list row row)
+  tt = unH1Record (ttRecord :: H1Record list row row)
+  conj l = conjRecord (H2Record l :: H2Record list row)
+  disj l = disjRecord (H2Record l :: H2Record list row)
+  implies l = impliesRecord (H2Record l :: H2Record list row)
+  not l = notRecord (H2Record l :: H2Record list row)
 
 foreign import boolConj :: Boolean -> Boolean -> Boolean
 foreign import boolDisj :: Boolean -> Boolean -> Boolean
 foreign import boolNot :: Boolean -> Boolean
 
+newtype H1Record :: RL.RowList Type -> Row Type -> Row Type -> Type
+newtype H1Record rowlist row subrow = H1Record { | subrow }
+
+unH1Record :: forall rowlist row subrow. H1Record rowlist row subrow -> { | subrow }
+unH1Record (H1Record r) = r
+
+newtype H2Record :: RL.RowList Type -> Row Type -> Type
+newtype H2Record rowlist row = H2Record { | row }
+
 -- | A class for records where all fields have `HeytingAlgebra` instances, used
 -- | to implement the `HeytingAlgebra` instance for records.
 class HeytingAlgebraRecord :: RL.RowList Type -> Row Type -> Row Type -> Constraint
 class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow where
-  ffRecord :: Proxy rowlist -> Proxy row -> Record subrow
-  ttRecord :: Proxy rowlist -> Proxy row -> Record subrow
-  impliesRecord :: Proxy rowlist -> Record row -> Record row -> Record subrow
-  disjRecord :: Proxy rowlist -> Record row -> Record row -> Record subrow
-  conjRecord :: Proxy rowlist -> Record row -> Record row -> Record subrow
-  notRecord :: Proxy rowlist -> Record row -> Record subrow
+  ffRecord :: H1Record rowlist row subrow
+  ttRecord :: H1Record rowlist row subrow
+  impliesRecord :: H2Record rowlist row -> Record row -> Record subrow
+  disjRecord :: H2Record rowlist row -> Record row -> Record subrow
+  conjRecord :: H2Record rowlist row -> Record row -> Record subrow
+  notRecord :: H2Record rowlist row -> Record subrow
 
 instance heytingAlgebraRecordNil :: HeytingAlgebraRecord RL.Nil row () where
-  conjRecord _ _ _ = {}
-  disjRecord _ _ _ = {}
-  ffRecord _ _ = {}
-  impliesRecord _ _ _ = {}
-  notRecord _ _ = {}
-  ttRecord _ _ = {}
+  conjRecord _ _ = {}
+  disjRecord _ _ = {}
+  ffRecord = H1Record {}
+  impliesRecord _ _ = {}
+  notRecord _ = {}
+  ttRecord = H1Record {}
 
 instance heytingAlgebraRecordCons ::
   ( IsSymbol key
@@ -130,42 +141,42 @@ instance heytingAlgebraRecordCons ::
   , HeytingAlgebra focus
   ) =>
   HeytingAlgebraRecord (RL.Cons key focus rowlistTail) row subrow where
-  conjRecord _ ra rb = insert (conj (get ra) (get rb)) tail
+  conjRecord (H2Record ra) rb = insert (conj (get ra) (get rb)) tail
     where
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = conjRecord (Proxy :: Proxy rowlistTail) ra rb
+    tail = conjRecord (H2Record ra :: H2Record rowlistTail row) rb
 
-  disjRecord _ ra rb = insert (disj (get ra) (get rb)) tail
+  disjRecord (H2Record ra) rb = insert (disj (get ra) (get rb)) tail
     where
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = disjRecord (Proxy :: Proxy rowlistTail) ra rb
+    tail = disjRecord (H2Record ra :: H2Record rowlistTail row) rb
 
-  impliesRecord _ ra rb = insert (implies (get ra) (get rb)) tail
+  impliesRecord (H2Record ra) rb = insert (implies (get ra) (get rb)) tail
     where
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = impliesRecord (Proxy :: Proxy rowlistTail) ra rb
+    tail = impliesRecord (H2Record ra :: H2Record rowlistTail row) rb
 
-  ffRecord _ row = insert ff tail
+  ffRecord = H1Record (insert ff tail)
     where
     key = reflectSymbol (Proxy :: Proxy key)
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = ffRecord (Proxy :: Proxy rowlistTail) row
+    tail = unH1Record (ffRecord :: H1Record rowlistTail row subrowTail)
 
-  notRecord _ row = insert (not (get row)) tail
+  notRecord (H2Record r) = insert (not (get r)) tail
     where
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = notRecord (Proxy :: Proxy rowlistTail) row
+    tail = notRecord (H2Record r :: H2Record rowlistTail row)
 
-  ttRecord _ row = insert tt tail
+  ttRecord = H1Record (insert tt tail)
     where
     key = reflectSymbol (Proxy :: Proxy key)
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = ttRecord (Proxy :: Proxy rowlistTail) row
+    tail = unH1Record (ttRecord :: H1Record rowlistTail row subrowTail)

src/Data/Monoid.purs

@@ -4,6 +4,7 @@ module Data.Monoid
   , power
   , guard
   , module Data.Semigroup
+  , MRecord
   , class MonoidRecord
   , memptyRecord
   ) where
@@ -62,7 +63,7 @@ instance monoidArray :: Monoid (Array a) where
   mempty = []
 
 instance monoidRecord :: (RL.RowToList row list, MonoidRecord list row row) => Monoid (Record row) where
-  mempty = memptyRecord (Proxy :: Proxy list)
+  mempty = unMRecord (memptyRecord :: MRecord list row)
 
 -- | Append a value to itself a certain number of times. For the
 -- | `Multiplicative` type, and for a non-negative power, this is the same as
@@ -97,14 +98,20 @@ guard :: forall m. Monoid m => Boolean -> m -> m
 guard true a = a
 guard false _ = mempty
 
+newtype MRecord :: RL.RowList Type -> Row Type -> Type
+newtype MRecord rowlist subrow = MRecord { | subrow }
+
+unMRecord :: forall rowlist subrow. MRecord rowlist subrow -> { | subrow }
+unMRecord (MRecord r) = r
+
 -- | A class for records where all fields have `Monoid` instances, used to
 -- | implement the `Monoid` instance for records.
 class MonoidRecord :: RL.RowList Type -> Row Type -> Row Type -> Constraint
 class SemigroupRecord rowlist row subrow <= MonoidRecord rowlist row subrow | rowlist -> row subrow where
-  memptyRecord :: Proxy rowlist -> Record subrow
+  memptyRecord :: MRecord rowlist subrow
 
 instance monoidRecordNil :: MonoidRecord RL.Nil row () where
-  memptyRecord _ = {}
+  memptyRecord = MRecord {}
 
 instance monoidRecordCons ::
   ( IsSymbol key
@@ -113,8 +120,8 @@ instance monoidRecordCons ::
   , MonoidRecord rowlistTail row subrowTail
   ) =>
   MonoidRecord (RL.Cons key focus rowlistTail) row subrow where
-  memptyRecord _ = insert mempty tail
+  memptyRecord = MRecord (insert mempty tail)
     where
     key = reflectSymbol (Proxy :: Proxy key)
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
-    tail = memptyRecord (Proxy :: Proxy rowlistTail)
+    tail = unMRecord (memptyRecord :: MRecord rowlistTail subrowTail)

src/Data/Ord.purs

@@ -19,6 +19,7 @@ module Data.Ord
   , abs
   , signum
   , module Data.Ordering
+  , ORecord
   , class OrdRecord
   , compareRecord
   ) where
@@ -234,12 +235,15 @@ class Eq1 f <= Ord1 f where
 instance ord1Array :: Ord1 Array where
   compare1 = compare
 
+newtype ORecord :: RL.RowList Type -> Row Type -> Type
+newtype ORecord rowlist row = ORecord { | row }
+
 class OrdRecord :: RL.RowList Type -> Row Type -> Constraint
 class EqRecord rowlist row <= OrdRecord rowlist row where
-  compareRecord :: Proxy rowlist -> Record row -> Record row -> Ordering
+  compareRecord :: ORecord rowlist row -> Record row -> Ordering
 
 instance ordRecordNil :: OrdRecord RL.Nil row where
-  compareRecord _ _ _ = EQ
+  compareRecord _ _ = EQ
 
 instance ordRecordCons ::
   ( OrdRecord rowlistTail row
@@ -248,9 +252,9 @@ instance ordRecordCons ::
   , Ord focus
   ) =>
   OrdRecord (RL.Cons key focus rowlistTail) row where
-  compareRecord _ ra rb =
+  compareRecord (ORecord ra) rb =
     if left /= EQ then left
-    else compareRecord (Proxy :: Proxy rowlistTail) ra rb
+    else compareRecord (ORecord ra :: ORecord rowlistTail row) rb
     where
     key = reflectSymbol (Proxy :: Proxy key)
     unsafeGet' = unsafeGet :: String -> Record row -> focus
@@ -261,4 +265,4 @@ instance ordRecord ::
   , OrdRecord list row
   ) =>
   Ord (Record row) where
-  compare = compareRecord (Proxy :: Proxy list)
+  compare l = compareRecord (ORecord l :: ORecord list row)

src/Data/Ring.purs

@@ -4,6 +4,7 @@ module Data.Ring
   , negate
   , (-)
   , module Data.Semiring
+  , RRecord
   , class RingRecord
   , subRecord
   ) where
@@ -45,7 +46,7 @@ instance ringProxy :: Ring (Proxy a) where
   sub _ _ = Proxy
 
 instance ringRecord :: (RL.RowToList row list, RingRecord list row row) => Ring (Record row) where
-  sub = subRecord (Proxy :: Proxy list)
+  sub l = subRecord (RRecord l :: RRecord list row)
 
 -- | `negate x` can be used as a shorthand for `zero - x`.
 negate :: forall a. Ring a => a -> a
@@ -54,14 +55,17 @@ negate a = zero - a
 foreign import intSub :: Int -> Int -> Int
 foreign import numSub :: Number -> Number -> Number
 
+newtype RRecord :: RL.RowList Type -> Row Type -> Type
+newtype RRecord rowlist row = RRecord { | row }
+
 -- | A class for records where all fields have `Ring` instances, used to
 -- | implement the `Ring` instance for records.
 class RingRecord :: RL.RowList Type -> Row Type -> Row Type -> Constraint
 class SemiringRecord rowlist row subrow <= RingRecord rowlist row subrow | rowlist -> subrow where
-  subRecord :: Proxy rowlist -> Record row -> Record row -> Record subrow
+  subRecord :: RRecord rowlist row -> Record row -> Record subrow
 
 instance ringRecordNil :: RingRecord RL.Nil row () where
-  subRecord _ _ _ = {}
+  subRecord _ _ = {}
 
 instance ringRecordCons ::
   ( IsSymbol key
@@ -70,9 +74,9 @@ instance ringRecordCons ::
   , Ring focus
   ) =>
   RingRecord (RL.Cons key focus rowlistTail) row subrow where
-  subRecord _ ra rb = insert (get ra - get rb) tail
+  subRecord (RRecord ra) rb = insert (get ra - get rb) tail
     where
     insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
     key = reflectSymbol (Proxy :: Proxy key)
     get = unsafeGet key :: Record row -> focus
-    tail = subRecord (Proxy :: Proxy rowlistTail) ra rb
+    tail = subRecord (RRecord ra :: RRecord rowlistTail row) rb