[ re #2960 ] Move defs of closures data types to a separate module

libs/base/Control/Relation.idr

@@ -127,59 +127,3 @@ PartialEquivalence ty Equal where
 
 public export
 Equivalence ty Equal where
-
-----------------------------------------
-
-public export
-data SymClosure : Rel ty -> ty -> ty -> Type where
-  Fwd : {0 x, y : ty} -> rel x y -> SymClosure rel x y
-  Bwd : {0 x, y : ty} -> rel y x -> SymClosure rel x y
-
-public export
-Reflexive ty rel => Reflexive ty (SymClosure rel) where
-  reflexive = Fwd reflexive
-
-public export
-Symmetric ty (SymClosure rel) where
-  symmetric (Fwd xy) = Bwd xy
-  symmetric (Bwd yx) = Fwd yx
-
-----------------------------------------
-
-public export
-data TransClosure : Rel ty -> ty -> ty -> Type where
-  Nil : TransClosure rel x x
-  (::) : {y : ty} -> rel x y -> TransClosure rel y z -> TransClosure rel x z
-
-public export
-Reflexive ty (TransClosure rel) where
-  reflexive = []
-
-public export
-Symmetric ty rel => Symmetric ty (TransClosure rel) where
-  symmetric {x} {y} xy = reverseOnto [] xy
-    where
-      reverseOnto : {z : ty} ->
-                    TransClosure rel z x ->
-                    TransClosure rel z y ->
-                    TransClosure rel y x
-      reverseOnto zx [] = zx
-      reverseOnto zx (zw :: wy) = reverseOnto (symmetric zw :: zx) wy
-
-public export
-Transitive ty (TransClosure rel) where
-  transitive [] yz = yz
-  transitive (xw :: wy) yz = xw :: transitive wy yz
-
-public export
-Symmetric ty rel => Euclidean ty (TransClosure rel) where
-  euclidean = euclidean @{TSE}
-
-public export
-Symmetric ty rel => Tolerance ty (TransClosure rel) where
-
-public export
-Symmetric ty rel => PartialEquivalence ty (TransClosure rel) where
-
-public export
-Symmetric ty rel => Equivalence ty (TransClosure rel) where

libs/base/Control/Relation/Closure.idr

@@ -0,0 +1,59 @@
+module Control.Relation.Closure
+
+import Control.Relation
+
+%default total
+
+public export
+data SymClosure : Rel ty -> ty -> ty -> Type where
+  Fwd : {0 x, y : ty} -> rel x y -> SymClosure rel x y
+  Bwd : {0 x, y : ty} -> rel y x -> SymClosure rel x y
+
+public export
+Reflexive ty rel => Reflexive ty (SymClosure rel) where
+  reflexive = Fwd reflexive
+
+public export
+Symmetric ty (SymClosure rel) where
+  symmetric (Fwd xy) = Bwd xy
+  symmetric (Bwd yx) = Fwd yx
+
+----------------------------------------
+
+public export
+data TransClosure : Rel ty -> ty -> ty -> Type where
+  Nil  : TransClosure rel x x
+  (::) : {y : ty} -> rel x y -> TransClosure rel y z -> TransClosure rel x z
+
+public export
+Reflexive ty (TransClosure rel) where
+  reflexive = []
+
+public export
+Symmetric ty rel => Symmetric ty (TransClosure rel) where
+  symmetric {x} {y} xy = reverseOnto [] xy
+    where
+      reverseOnto : {z : ty} ->
+                    TransClosure rel z x ->
+                    TransClosure rel z y ->
+                    TransClosure rel y x
+      reverseOnto zx [] = zx
+      reverseOnto zx (zw :: wy) = reverseOnto (symmetric zw :: zx) wy
+
+public export
+Transitive ty (TransClosure rel) where
+  transitive [] yz = yz
+  transitive (xw :: wy) yz = xw :: transitive wy yz
+
+public export
+Symmetric ty rel => Euclidean ty (TransClosure rel) where
+  euclidean = euclidean @{TSE}
+
+public export
+Symmetric ty rel => Tolerance ty (TransClosure rel) where
+
+public export
+Symmetric ty rel => PartialEquivalence ty (TransClosure rel) where
+
+public export
+Symmetric ty rel => Equivalence ty (TransClosure rel) where

libs/base/Data/List.idr

@@ -906,12 +906,12 @@ groupAllWith f = groupWith f . sortBy (comparing f)
 
 -- Nil is not Cons
 export
-{0 xs : List a} -> Uninhabited ([] = x :: xs) where
+Uninhabited ([] = x :: xs) where
   uninhabited Refl impossible
 
 -- Cons is not Nil
 export
-{0 xs : List a} -> Uninhabited (x :: xs = []) where
+Uninhabited (x :: xs = []) where
   uninhabited Refl impossible
 
 -- If the heads or the tails of two lists are provably non-equal, then the

tests/idris2/basic044/expected

@@ -109,25 +109,21 @@ LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
   ($resolvedN 2)
   ($resolvedN 2)
 With default. Target type : Prelude.Types.Nat
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
-(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
 (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
 (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
 (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
 Target type : ({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat)
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
-$resolvedN
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
 $resolvedN
 $resolvedN
 Target type : ?Vec.{a:N}_[]
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
-(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
 (($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
 (($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
 (($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
 Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
-(($resolvedN (fromInteger 0)) Nil)
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
 (($resolvedN (fromInteger 0)) Nil)
 (($resolvedN (fromInteger 0)) Nil)
 (($resolvedN (fromInteger 0)) Nil)
@@ -136,32 +132,26 @@ LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
   ($resolvedN 0)
   ($resolvedN 0)
 With default. Target type : ?Vec.{a:N}_[]
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
-$resolvedN
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
 $resolvedN
 $resolvedN
 Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
-LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
-  ($resolvedN 0)
-  ($resolvedN 0)
-With default. Target type : (?Vec.{rel:N}_[] ?Vec.{x:N}_[] ?Vec.{y:N}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
   ($resolvedN 0)
   ($resolvedN 0)
 With default. Target type : ?Vec.{a:N}_[]
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
-$resolvedN
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
 $resolvedN
 $resolvedN
 Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 4 candidates) (delayed) at Vec:L:C--L:C:
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
 (($resolvedN (fromInteger 0)) Nil)
 Target type : (Prelude.Basics.List Prelude.Types.Nat)
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
   ($resolvedN 0)
   ($resolvedN 0)
 With default. Target type : Prelude.Types.Nat
-LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
+LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:L:C--L:C:
 $resolvedN
 Target type : (Prelude.Basics.List Prelude.Types.Nat)
 LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))

tests/idris2/with003/expected

@@ -14,7 +14,6 @@ Main> Error: Can't find an implementation for Num ().
                                                                 ^^^^
 
 Main> Error: Ambiguous elaboration. Possible results:
-    Control.Relation.Nil
     Prelude.Nil
     Data.Vect.Nil