fix universe issues with EnumType

lecopivo · Sep 4, 2023 · bed4125 · bed4125
1 parent c4b9e8e
commit bed4125
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/SciLean/Core/Objects/SemiInnerProductSpace.lean b/SciLean/Core/Objects/SemiInnerProductSpace.lean
@@ -75,7 +75,7 @@ instance (K X Y) [AddCommMonoid K] [Inner K X] [Inner K Y] : Inner K (X × Y) wh
 -- instance (K X) [AddCommMonoid K] [Inner K X] (ι) [EnumType ι] : Inner K (ι → X) where
 --   inner := λ f g => EnumType.sum fun i => ⟪f i, g i⟫[K]
 
-instance (priority:=low) (K ι) (X : ι → Type) 
+instance (priority:=low) (K ι) (X : ι → Type _) 
   [AddCommMonoid K] [∀ i, Inner K (X i)] [EnumType ι] 
   : Inner K ((i : ι) → X i) where
   inner := λ f g => ∑ i, ⟪f i, g i⟫[K]
@@ -102,7 +102,7 @@ instance (X Y) [TestFunctions X] [TestFunctions Y] : TestFunctions (X×Y) where
 -- instance (X ι : Type _) [TestFunctions X]  : TestFunctions (ι → X) where
 --   TestFunction f := ∀ i, TestFunction (f i)
 
-instance (priority:=low) (ι : Type _) (X : ι → Type) [∀ i, TestFunctions (X i)]
+instance (priority:=low) (ι : Type _) (X : ι → Type _) [∀ i, TestFunctions (X i)]
   : TestFunctions ((i : ι) → X i) where
   TestFunction f := ∀ i, TestFunction (f i)
 
@@ -225,6 +225,6 @@ instance (X Y) [SemiInnerProductSpace K X] [SemiInnerProductSpace K Y] : SemiInn
 
 -- instance (X) [SemiInnerProductSpace K X] (ι) [Fintype ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
 -- instance (X) [SemiInnerProductSpace K X] (ι) [EnumType ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
-instance (priority:=low) (ι) (X : ι → Type) [∀ i, SemiInnerProductSpace K (X i)] [EnumType ι] : SemiInnerProductSpace K ((i : ι) → X i) 
+instance (priority:=low) (ι) (X : ι → Type _) [∀ i, SemiInnerProductSpace K (X i)] [EnumType ι] : SemiInnerProductSpace K ((i : ι) → X i) 
   := SemiInnerProductSpace.mkSorryProofs
 
diff --git a/SciLean/Data/EnumType.lean b/SciLean/Data/EnumType.lean
@@ -16,7 +16,7 @@ class EnumType (ι : Type u) where
 
   -- Ther return type has `ForInStep` because it is useful to know if the loop 
   -- ended normall or if it was interupted. This way we can easily exit from nested loops
-  forIn {m : Type → Type} [Monad m] {β : Type} (init : β) (f : ι → β → m (ForInStep β)) : m (ForInStep β)
+  forIn {m : Type v → Type w} [Monad m] {β : Type v} (init : β) (f : ι → β → m (ForInStep β)) : m (ForInStep β)
 
   -- something that foldM runs over all elements
 

diff --git a/test/basic_gradients.lean b/test/basic_gradients.lean
@@ -8,11 +8,11 @@ import SciLean.Core.Simp.Sum
 open SciLean
 
 variable 
-  {K : Type} [RealScalar K]
-  {X : Type} [SemiInnerProductSpace K X]
-  {Y : Type} [SemiInnerProductSpace K Y]
-  {Z : Type} [SemiInnerProductSpace K Z]
-  {ι : Type} [EnumType ι]
+  {K : Type _} [RealScalar K]
+  {X : Type _} [SemiInnerProductSpace K X]
+  {Y : Type _} [SemiInnerProductSpace K Y]
+  {Z : Type _} [SemiInnerProductSpace K Z]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
 set_default_scalar K