New (simpler but more robust) implementation of canonicity check

lib/Haskell/Prim/Applicative.agda

@@ -41,43 +41,52 @@ record DefaultApplicative (f : Set → Set) : Set₁ where
 open Applicative ⦃...⦄ public
 {-# COMPILE AGDA2HS Applicative existing-class #-}
 -- ** instances
-private
-  mkApplicative : DefaultApplicative t → Applicative t
-  mkApplicative x = record {DefaultApplicative x}
 instance
   open DefaultApplicative
 
+  iDefaultApplicativeList : DefaultApplicative List
+  iDefaultApplicativeList .pure x = x ∷ []
+  iDefaultApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs
+
   iApplicativeList : Applicative List
-  iApplicativeList = mkApplicative λ where
-    .pure x      → x ∷ []
-    ._<*>_ fs xs → concatMap (λ f → map f xs) fs
+  iApplicativeList = record {DefaultApplicative iDefaultApplicativeList}
+
+  iDefaultApplicativeMaybe : DefaultApplicative Maybe
+  iDefaultApplicativeMaybe .pure = Just
+  iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
+  iDefaultApplicativeMaybe ._<*>_ _        _        = Nothing
 
   iApplicativeMaybe : Applicative Maybe
-  iApplicativeMaybe = mkApplicative λ where
-    .pure → Just
-    ._<*>_ (Just f) (Just x) → Just (f x)
-    ._<*>_ _        _        → Nothing
+  iApplicativeMaybe = record {DefaultApplicative iDefaultApplicativeMaybe}
+
+  iDefaultApplicativeEither : DefaultApplicative (Either a)
+  iDefaultApplicativeEither .pure = Right
+  iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
+  iDefaultApplicativeEither ._<*>_ (Left e)  _         = Left e
+  iDefaultApplicativeEither ._<*>_ _         (Left e)  = Left e
 
   iApplicativeEither : Applicative (Either a)
-  iApplicativeEither = mkApplicative λ where
-    .pure → Right
-    ._<*>_ (Right f) (Right x) → Right (f x)
-    ._<*>_ (Left e)  _         → Left e
-    ._<*>_ _         (Left e)  → Left e
+  iApplicativeEither = record{DefaultApplicative iDefaultApplicativeEither}
+
+  iDefaultApplicativeFun : DefaultApplicative (λ b → a → b)
+  iDefaultApplicativeFun .pure        = const
+  iDefaultApplicativeFun ._<*>_ f g x = f x (g x)
 
   iApplicativeFun : Applicative (λ b → a → b)
-  iApplicativeFun = mkApplicative λ where
-    .pure        → const
-    ._<*>_ f g x → f x (g x)
+  iApplicativeFun = record{DefaultApplicative iDefaultApplicativeFun}
+
+  iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → DefaultApplicative (a ×_)
+  iDefaultApplicativeTuple₂ .pure x                = mempty , x
+  iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x
 
   iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
-  iApplicativeTuple₂ = mkApplicative λ where
-    .pure x                → mempty , x
-    ._<*>_ (a , f) (b , x) → a <> b , f x
+  iApplicativeTuple₂ = record{DefaultApplicative iDefaultApplicativeTuple₂}
+
+  iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultApplicative (a × b ×_)
+  iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x
+  iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x
 
   iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
-  iApplicativeTuple₃ = mkApplicative λ where
-    .pure x                → mempty , mempty , x
-    ._<*>_ (a , u , f) (b , v , x) → a <> b , u <> v , f x
+  iApplicativeTuple₃ = record{DefaultApplicative iDefaultApplicativeTuple₃}
 
 instance postulate iApplicativeIO : Applicative IO

lib/Haskell/Prim/Enum.agda

@@ -122,82 +122,142 @@ instance
   iEnumInteger .enumFromTo        = integerFromTo
   iEnumInteger .enumFromThenTo    = integerFromThenTo
 
-module _ (from : a → Integer) (to : Integer → a) where
-  private
-    fromTo : a → a → List a
-    fromTo a b = map to (enumFromTo (from a) (from b))
-
-    fromThenTo : (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
-    fromThenTo a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
-
-  unboundedEnumViaInteger : Enum a
-  unboundedEnumViaInteger .BoundedBelowEnum      = Nothing
-  unboundedEnumViaInteger .BoundedAboveEnum      = Nothing
-  unboundedEnumViaInteger .fromEnum              = integerToInt ∘ from
-  unboundedEnumViaInteger .toEnum         n      = to (intToInteger n)
-  unboundedEnumViaInteger .succ           x      = to (from x + 1)
-  unboundedEnumViaInteger .pred           x      = to (from x - 1)
-  unboundedEnumViaInteger .enumFromTo     a b    = fromTo a b
-  unboundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedBelowEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedBelow a ⦄ → Enum a
-  boundedBelowEnumViaInteger .BoundedBelowEnum      = Just it
-  boundedBelowEnumViaInteger .BoundedAboveEnum      = Nothing
-  boundedBelowEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedBelowEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedBelowEnumViaInteger .succ           x      = to (from x + 1)
-  boundedBelowEnumViaInteger .pred           x      = to (from x - 1)
-  boundedBelowEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedBelowEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedAboveEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedAbove a ⦄ → Enum a
-  boundedAboveEnumViaInteger .BoundedBelowEnum      = Nothing
-  boundedAboveEnumViaInteger .BoundedAboveEnum      = Just it
-  boundedAboveEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedAboveEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedAboveEnumViaInteger .succ           x      = to (from x + 1)
-  boundedAboveEnumViaInteger .pred           x      = to (from x - 1)
-  boundedAboveEnumViaInteger .enumFrom       a      = fromTo a maxBound
-  boundedAboveEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedAboveEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedEnumViaInteger : ⦃ Ord a ⦄ → ⦃ Bounded a ⦄ → Enum a
-  boundedEnumViaInteger .BoundedBelowEnum      = Just it
-  boundedEnumViaInteger .BoundedAboveEnum      = Just it
-  boundedEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedEnumViaInteger .succ           x      = to (from x + 1)
-  boundedEnumViaInteger .pred           x      = to (from x - 1)
-  boundedEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-  boundedEnumViaInteger .enumFrom       a      = fromTo a maxBound
-  boundedEnumViaInteger .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo a a₁ maxBound
-              else fromThenTo a a₁ minBound
+private
+  fromTo : (from : a → Integer) (to : Integer → a)
+         → a → a → List a
+  fromTo from to a b = map to (enumFromTo (from a) (from b))
+
+  fromThenTo : (from : a → Integer) (to : Integer → a)
+             → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
+  fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
+
 
 instance
   iEnumNat : Enum Nat
-  iEnumNat = boundedBelowEnumViaInteger pos unsafeIntegerToNat
+  iEnumNat .BoundedBelowEnum = Just it
+  iEnumNat .BoundedAboveEnum = Nothing
+  iEnumNat .fromEnum = integerToInt ∘ pos
+  iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n)
+  iEnumNat .succ n = suc n
+  iEnumNat .pred (suc n) = n
+  iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat
+  iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat
 
   iEnumInt : Enum Int
-  iEnumInt = boundedEnumViaInteger intToInteger integerToInt
+  iEnumInt .BoundedBelowEnum      = Just it
+  iEnumInt .BoundedAboveEnum      = Just it
+  iEnumInt .fromEnum              = integerToInt ∘ intToInteger
+  iEnumInt .toEnum         n      = integerToInt (intToInteger n)
+  iEnumInt .succ           x      = integerToInt (intToInteger x + 1)
+  iEnumInt .pred           x      = integerToInt (intToInteger x - 1)
+  iEnumInt .enumFromTo     a b    = fromTo intToInteger integerToInt a b
+  iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b
+  iEnumInt .enumFrom       a      = fromTo intToInteger integerToInt a maxBound
+  iEnumInt .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound
+              else fromThenTo intToInteger integerToInt a a₁ minBound
 
   iEnumWord : Enum Word
-  iEnumWord = boundedEnumViaInteger wordToInteger integerToWord
+  iEnumWord .BoundedBelowEnum      = Just it
+  iEnumWord .BoundedAboveEnum      = Just it
+  iEnumWord .fromEnum              = integerToInt ∘ wordToInteger
+  iEnumWord .toEnum         n      = integerToWord (intToInteger n)
+  iEnumWord .succ           x      = integerToWord (wordToInteger x + 1)
+  iEnumWord .pred           x      = integerToWord (wordToInteger x - 1)
+  iEnumWord .enumFromTo     a b    = fromTo wordToInteger integerToWord a b
+  iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b
+  iEnumWord .enumFrom       a      = fromTo wordToInteger integerToWord a maxBound
+  iEnumWord .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound
+              else fromThenTo wordToInteger integerToWord a a₁ minBound
+
+private
+  fromBool : Bool → Integer
+  fromBool = if_then 1 else 0
+
+  toBool : Integer → Bool
+  toBool = _/= 0
 
+instance
   iEnumBool : Enum Bool
-  iEnumBool = boundedEnumViaInteger (if_then 1 else 0) (_/= 0)
+  iEnumBool .BoundedBelowEnum      = Just it
+  iEnumBool .BoundedAboveEnum      = Just it
+  iEnumBool .fromEnum              = integerToInt ∘ fromBool
+  iEnumBool .toEnum         n      = toBool (intToInteger n)
+  iEnumBool .succ           x      = toBool (fromBool x + 1)
+  iEnumBool .pred           x      = toBool (fromBool x - 1)
+  iEnumBool .enumFromTo     a b    = fromTo fromBool toBool a b
+  iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b
+  iEnumBool .enumFrom       a      = fromTo fromBool toBool a maxBound
+  iEnumBool .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound
+              else fromThenTo fromBool toBool a a₁ minBound
+
+private
+  fromOrdering : Ordering → Integer
+  fromOrdering = λ where LT → 0; EQ → 1; GT → 2
 
+  toOrdering : Integer → Ordering
+  toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT
+
+instance
   iEnumOrdering : Enum Ordering
-  iEnumOrdering = boundedEnumViaInteger (λ where LT → 0; EQ → 1; GT → 2)
-                                        (λ where (pos 0) → LT; (pos 1) → EQ; _ → GT)
+  iEnumOrdering .BoundedBelowEnum      = Just it
+  iEnumOrdering .BoundedAboveEnum      = Just it
+  iEnumOrdering .fromEnum              = integerToInt ∘ fromOrdering
+  iEnumOrdering .toEnum         n      = toOrdering (intToInteger n)
+  iEnumOrdering .succ           x      = toOrdering (fromOrdering x + 1)
+  iEnumOrdering .pred           x      = toOrdering (fromOrdering x - 1)
+  iEnumOrdering .enumFromTo     a b    = fromTo fromOrdering toOrdering a b
+  iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b
+  iEnumOrdering .enumFrom       a      = fromTo fromOrdering toOrdering a maxBound
+  iEnumOrdering .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound
+              else fromThenTo fromOrdering toOrdering a a₁ minBound
+
+private
+  fromUnit : ⊤ → Integer
+  fromUnit _ = 0
+
+  toUnit : Integer → ⊤
+  toUnit _ = tt
 
+instance
   iEnumUnit : Enum ⊤
-  iEnumUnit = boundedEnumViaInteger (λ _ → 0) λ _ → tt
+  iEnumUnit .BoundedBelowEnum      = Just it
+  iEnumUnit .BoundedAboveEnum      = Just it
+  iEnumUnit .fromEnum              = integerToInt ∘ fromUnit
+  iEnumUnit .toEnum         n      = toUnit (intToInteger n)
+  iEnumUnit .succ           x      = toUnit (fromUnit x + 1)
+  iEnumUnit .pred           x      = toUnit (fromUnit x - 1)
+  iEnumUnit .enumFromTo     a b    = fromTo fromUnit toUnit a b
+  iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b
+  iEnumUnit .enumFrom       a      = fromTo fromUnit toUnit a maxBound
+  iEnumUnit .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound
+              else fromThenTo fromUnit toUnit a a₁ minBound
+
+private
+  fromChar : Char → Integer
+  fromChar = pos ∘ c2n
 
+  toChar : Integer → Char
+  toChar = λ where (pos n) → primNatToChar n; _ → '_'
+
+instance
   iEnumChar : Enum Char
-  iEnumChar = boundedEnumViaInteger (pos ∘ c2n)
-                                    λ where (pos n) → primNatToChar n; _ → '_'
+  iEnumChar .BoundedBelowEnum      = Just it
+  iEnumChar .BoundedAboveEnum      = Just it
+  iEnumChar .fromEnum              = integerToInt ∘ fromChar
+  iEnumChar .toEnum         n      = toChar (intToInteger n)
+  iEnumChar .succ           x      = toChar (fromChar x + 1)
+  iEnumChar .pred           x      = toChar (fromChar x - 1)
+  iEnumChar .enumFromTo     a b    = fromTo fromChar toChar a b
+  iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b
+  iEnumChar .enumFrom       a      = fromTo fromChar toChar a maxBound
+  iEnumChar .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound
+              else fromThenTo fromChar toChar a a₁ minBound
 
   -- Missing:
   --  Enum Double  (can't go via Integer)

lib/Haskell/Prim/Foldable.agda

@@ -88,29 +88,35 @@ open Foldable ⦃...⦄ public
 {-# COMPILE AGDA2HS Foldable existing-class #-}
 
 -- ** instances
-private
-  mkFoldable : DefaultFoldable t → Foldable t
-  mkFoldable x = record {DefaultFoldable x}
-
-  foldMap=_ : (∀ {b a} → ⦃ Monoid b ⦄ → (a → b) → t a → b) → Foldable t
-  foldMap= x = record {DefaultFoldable (record {foldMap = x})}
 instance
-  iFoldableList : Foldable List
-  iFoldableList = foldMap= foldMapList
+  iDefaultFoldableList : DefaultFoldable List
+  iDefaultFoldableList .DefaultFoldable.foldMap = foldMapList
     where
       foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
       foldMapList f []       = mempty
       foldMapList f (x ∷ xs) = f x <> foldMapList f xs
 
-  iFoldableMaybe : Foldable Maybe
-  iFoldableMaybe = foldMap= λ where
+  iFoldableList : Foldable List
+  iFoldableList = record {DefaultFoldable iDefaultFoldableList}
+
+  iDefaultFoldableMaybe : DefaultFoldable Maybe
+  iDefaultFoldableMaybe .DefaultFoldable.foldMap = λ where
     _ Nothing  → mempty
     f (Just x) → f x
 
-  iFoldableEither : Foldable (Either a)
-  iFoldableEither = foldMap= λ where
+  iFoldableMaybe : Foldable Maybe
+  iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe}
+
+  iDefaultFoldableEither : DefaultFoldable (Either a)
+  iDefaultFoldableEither .DefaultFoldable.foldMap = λ where
     _ (Left _)  → mempty
     f (Right x) → f x
 
+  iFoldableEither : Foldable (Either a)
+  iFoldableEither = record {DefaultFoldable iDefaultFoldableEither}
+
+  iDefaultFoldablePair : DefaultFoldable (a ×_)
+  iDefaultFoldablePair .DefaultFoldable.foldMap = λ f (_ , x) → f x
+
   iFoldablePair : Foldable (a ×_)
-  iFoldablePair = foldMap= λ f (_ , x) → f x
+  iFoldablePair = record {DefaultFoldable iDefaultFoldablePair}

lib/Haskell/Prim/Functor.agda

@@ -45,34 +45,45 @@ void = tt <$_
 infixl 1 _<&>_
 infixl 4 _<$>_ _$>_
 
--- ** instances
-private
-  mkFunctor : DefaultFunctor t → Functor t
-  mkFunctor x = record {DefaultFunctor x}
-
-  fmap=_ : (∀ {a b} → (a → b) → f a → f b) → Functor f
-  fmap= x = record {DefaultFunctor (record {fmap = x})}
 instance
+  iDefaultFunctorList : DefaultFunctor List
+  iDefaultFunctorList .DefaultFunctor.fmap = map
+
   iFunctorList : Functor List
-  iFunctorList = fmap= map
+  iFunctorList = record{DefaultFunctor iDefaultFunctorList}
 
-  iFunctorMaybe : Functor Maybe
-  iFunctorMaybe = fmap= λ where
+  iDefaultFunctorMaybe : DefaultFunctor Maybe
+  iDefaultFunctorMaybe .DefaultFunctor.fmap = λ where
     f Nothing  → Nothing
     f (Just x) → Just (f x)
 
-  iFunctorEither : Functor (Either a)
-  iFunctorEither = fmap= λ where
+  iFunctorMaybe : Functor Maybe
+  iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe}
+
+  iDefaultFunctorEither : DefaultFunctor (Either a)
+  iDefaultFunctorEither .DefaultFunctor.fmap = λ where
     f (Left  x) → Left x
     f (Right y) → Right (f y)
 
+  iFunctorEither : Functor (Either a)
+  iFunctorEither = record{DefaultFunctor iDefaultFunctorEither}
+
+  iDefaultFunctorFun : DefaultFunctor (λ b → a → b)
+  iDefaultFunctorFun .DefaultFunctor.fmap = _∘_
+
   iFunctorFun : Functor (λ b → a → b)
-  iFunctorFun = fmap= _∘_
+  iFunctorFun = record{DefaultFunctor iDefaultFunctorFun}
+
+  iDefaultFunctorTuple₂ : DefaultFunctor (a ×_)
+  iDefaultFunctorTuple₂ .DefaultFunctor.fmap = λ f (x , y) → x , f y
 
   iFunctorTuple₂ : Functor (a ×_)
-  iFunctorTuple₂ = fmap= λ f (x , y) → x , f y
+  iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂}
+
+  iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_)
+  iDefaultFunctorTuple₃ .DefaultFunctor.fmap = λ where f (x , y , z) → x , y , f z
 
   iFunctorTuple₃ : Functor (a × b ×_)
-  iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z
+  iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃}
 
 instance postulate iFunctorIO : Functor IO