Skip to content

Instantly share code, notes, and snippets.

@mattrobball

mattrobball/trace.txt

Created August 17, 2023 17:54
Show Gist options
  • Save mattrobball/15f8c763eaa169195367d2745e5a8e22 to your computer and use it in GitHub Desktop.
Save mattrobball/15f8c763eaa169195367d2745e5a8e22 to your computer and use it in GitHub Desktop.
Download ZIP
TC synthesis trace with instFunlikeDual
Raw
trace.txt
cumulative profiling times:
attribute application 0.000958ms
compilation new 0.00383ms
interpretation 10.6ms
type checking 0.0395ms
typeclass inference 0.787ms
scratch.lean:6:4: warning: declaration uses 'sorry'
scratch.lean:6:4: warning: declaration uses 'sorry'
scratch.lean:11:4: warning: declaration uses 'sorry'
scratch.lean:11:4: warning: declaration uses 'sorry'
scratch.lean:21:43: error: function expected at
foo
term has type
?m.2142 →ₗ[?m.2142] ?m.2142
[Meta.isDefEq] [0.000004s] ✅ Sort ?u.2128 =?= Type ?u.2129
[Meta.isDefEq] [0.000001s] ✅ Type u_1 =?= Type u_1
[Meta.isDefEq] [0.000001s] ✅ Type ?u.2129 =?= Type u_1
[Meta.isDefEq] [0.000001s] ✅ Type u_1 =?= Type u_1
[Meta.isDefEq] [0.000001s] ✅ Sort ?u.2134 =?= Type ?u.2135
[Meta.isDefEq] [0.000001s] ✅ Type u_2 =?= Type u_2
[Meta.isDefEq] [0.000001s] ✅ Type ?u.2135 =?= Type u_2
[Meta.isDefEq] [0.000000s] ✅ Type u_2 =?= Type u_2
[Meta.isDefEq] [0.000001s] ✅ Sort ?u.2137 =?= Type u_2
[Meta.synthInstance] [0.000078s] 💥 Semiring ?m.2142
[Meta.synthInstance] [0.000033s] new goal Semiring ?m.2142
[Meta.synthInstance.instances] #[@SubsemiringClass.toSemiring, @instSemiring, @Ring.toSemiring, @CommSemiring.toSemiring, @DivisionSemiring.toSemiring, @OrderedSemiring.toSemiring, @StrictOrderedSemiring.toSemiring, @IdemSemiring.toSemiring, @Pi.semiring, @Matrix.semiring, Rat.semiring, MulOpposite.semiring, @ULift.semiring, AddOpposite.semiring, @Subsemiring.toSemiring, @Subalgebra.toSemiring, @RingCon.instSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMul, Int.instSemiringInt, @Module.End.semiring, instSemiringRestrictScalars, @WithZero.semiring, Nat.semiring, @AddMonoid.End.semiring, @Prod.instSemiring, inst✝]
[Meta.synthInstance] [0.000029s] 💥 apply inst✝ to Semiring ?m.2142
[Meta.synthInstance.tryResolve] [0.000022s] 💥 Semiring ?m.2142 ≟ Semiring R
[Meta.isDefEq] [0.000020s] 💥 Semiring ?m.2142 =?= Semiring R
[Meta.isDefEq] [0.000003s] 💥 ?m.2142 =?= R
[Meta.isDefEq] ?m.2142 [nonassignable] =?= R [nonassignable]
[Meta.synthInstance] [0.000700s] 💥 CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2177
[Meta.synthInstance] [0.000017s] new goal CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) _tc.0
[Meta.synthInstance.instances] #[@FunLike.hasCoeToFun]
[Meta.synthInstance] [0.000289s] ✅ apply @FunLike.hasCoeToFun to CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) fun x =>
(a : ?m.2184) → ?m.2185 a
[Meta.synthInstance.tryResolve] [0.000195s] ✅ CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) fun x =>
(a : ?m.2184) → ?m.2185 a ≟ CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) fun x => (a : ?m.2184) → ?m.2185 a
[Meta.isDefEq] [0.000124s] ✅ CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142)
?m.2178 =?= CoeFun ?m.2183 fun x => (a : ?m.2184) → ?m.2185 a
[Meta.isDefEq] [0.000017s] ✅ ?m.2142 →ₗ[?m.2142] ?m.2142 =?= ?m.2183
[Meta.isDefEq] ?m.2142 →ₗ[?m.2142] ?m.2142 [nonassignable] =?= ?m.2183 [assignable]
[Meta.isDefEq] [0.000001s] ✅ Sort ?u.2182 =?= Type ?u.2141
[Meta.isDefEq] [0.000061s] ✅ ?m.2178 =?= fun x => (a : ?m.2184) → ?m.2185 a
[Meta.isDefEq] ?m.2178 [assignable] =?= fun x => (a : ?m.2184) → ?m.2185 a [nonassignable]
[Meta.isDefEq] [0.000031s] ✅ outParam
((?m.2142 →ₗ[?m.2142] ?m.2142) →
Sort ?u.2176) =?= (?m.2142 →ₗ[?m.2142] ?m.2142) → Sort (imax ?u.2181 ?u.2180)
[Meta.isDefEq] [0.000006s] ✅ (?m.2142 →ₗ[?m.2142] ?m.2142) →
Sort ?u.2176 =?= (?m.2142 →ₗ[?m.2142] ?m.2142) → Sort (imax ?u.2181 ?u.2180)
[Meta.isDefEq] [0.000001s] ✅ ?m.2142 →ₗ[?m.2142] ?m.2142 =?= ?m.2142 →ₗ[?m.2142] ?m.2142
[Meta.isDefEq] [0.000002s] ✅ Sort ?u.2176 =?= Sort (imax ?u.2181 ?u.2180)
[Meta.isDefEq] [0.000065s] ✅ ?m.2179 =?= FunLike.hasCoeToFun
[Meta.isDefEq] ?m.2179 [assignable] =?= FunLike.hasCoeToFun [nonassignable]
[Meta.isDefEq] [0.000045s] ✅ CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) fun x =>
(a : ?m.2184) → ?m.2185 a =?= CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) fun x => (a : ?m.2184) → ?m.2185 a
[Meta.isDefEq] [0.000001s] ✅ ?m.2142 →ₗ[?m.2142] ?m.2142 =?= ?m.2142 →ₗ[?m.2142] ?m.2142
[Meta.isDefEq] [0.000001s] ✅ fun x => (a : ?m.2184) → ?m.2185 a =?= fun x => (a : ?m.2184) → ?m.2185 a
[Meta.synthInstance] [0.000057s] new goal FunLike (?m.2142 →ₗ[?m.2142] ?m.2142) _tc.2 _tc.3
[Meta.synthInstance.instances] #[@ZeroHomClass.toFunLike, @AddHomClass.toFunLike, @OneHomClass.toFunLike, @MulHomClass.toFunLike, @EmbeddingLike.toFunLike, @RelHomClass.toFunLike, @SMulHomClass.toFunLike, @StarHomClass.toFunLike, @TopHomClass.toFunLike, @BotHomClass.toFunLike, @SupHomClass.toFunLike, @InfHomClass.toFunLike, @NonnegHomClass.toFunLike, @SubadditiveHomClass.toFunLike, @SubmultiplicativeHomClass.toFunLike, @MulLEAddHomClass.toFunLike, @NonarchimedeanHomClass.toFunLike, @sSupHomClass.toFunLike, @sInfHomClass.toFunLike, @LinearMap.instFunLike, Module.Dual.instFunLikeDual]
[Meta.synthInstance] [0.000336s] 💥 apply Module.Dual.instFunLikeDual to FunLike (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2184
?m.2185
[Meta.synthInstance.tryResolve] [0.000296s] 💥 FunLike (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2184
?m.2185 ≟ FunLike (Module.Dual ?m.2262 ?m.2263) ?m.2263 fun x => ?m.2262
[Meta.isDefEq] [0.000292s] 💥 FunLike (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2184
?m.2185 =?= FunLike (Module.Dual ?m.2262 ?m.2263) ?m.2263 fun x => ?m.2262
[Meta.isDefEq] [0.000249s] 💥 ?m.2142 →ₗ[?m.2142] ?m.2142 =?= Module.Dual ?m.2262 ?m.2263
[Meta.isDefEq] [0.000216s] 💥 ?m.2142 →ₗ[?m.2142] ?m.2142 =?= ?m.2263 →ₗ[?m.2262] ?m.2262
[Meta.isDefEq] [0.000007s] ✅ ?m.2142 =?= ?m.2262
[Meta.isDefEq] ?m.2142 [nonassignable] =?= ?m.2262 [assignable]
[Meta.isDefEq] [0.000001s] ✅ Type ?u.2260 =?= Type ?u.2141
[Meta.isDefEq] [0.000162s] 💥 RingHom.id ?m.2142 =?= RingHom.id ?m.2142
[Meta.isDefEq] [0.000000s] ✅ ?m.2142 =?= ?m.2142
[Meta.isDefEq] [0.000135s] 💥 Semiring.toNonAssocSemiring =?= Semiring.toNonAssocSemiring
[Meta.isDefEq] [0.000000s] ✅ ?m.2142 =?= ?m.2142
[Meta.synthInstance] [0.000048s] 💥 Semiring ?m.2142
[Meta.synthInstance] [0.000022s] new goal Semiring ?m.2142
[Meta.synthInstance.instances] #[@SubsemiringClass.toSemiring, @instSemiring, @Ring.toSemiring, @CommSemiring.toSemiring, @DivisionSemiring.toSemiring, @OrderedSemiring.toSemiring, @StrictOrderedSemiring.toSemiring, @IdemSemiring.toSemiring, @Pi.semiring, @Matrix.semiring, Rat.semiring, MulOpposite.semiring, @ULift.semiring, AddOpposite.semiring, @Subsemiring.toSemiring, @Subalgebra.toSemiring, @RingCon.instSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMul, Int.instSemiringInt, @Module.End.semiring, instSemiringRestrictScalars, @WithZero.semiring, Nat.semiring, @AddMonoid.End.semiring, @Prod.instSemiring, inst✝]
[Meta.synthInstance] [0.000015s] 💥 apply inst✝ to Semiring ?m.2142
[Meta.synthInstance.tryResolve] [0.000010s] 💥 Semiring ?m.2142 ≟ Semiring R
[Meta.isDefEq] [0.000008s] 💥 Semiring ?m.2142 =?= Semiring R
[Meta.isDefEq] [0.000001s] 💥 ?m.2142 =?= R
[Meta.isDefEq] ?m.2142 [nonassignable] =?= R [nonassignable]
[Meta.synthInstance] [0.000053s] 💥 CommSemiring ?m.2142
[Meta.synthInstance] [0.000020s] new goal CommSemiring ?m.2142
[Meta.synthInstance.instances] #[@CommRing.toCommSemiring, @Semifield.toCommSemiring, @OrderedCommSemiring.toCommSemiring, @StrictOrderedCommSemiring.toCommSemiring, @CanonicallyOrderedCommSemiring.toCommSemiring, @IdemCommSemiring.toCommSemiring, @Pi.commSemiring, @WithBot.commSemiring, Cardinal.commSemiring, Rat.commSemiring, MulOpposite.commSemiring, @ULift.commSemiring, AddOpposite.commSemiring, @SubsemiringClass.toCommSemiring, @Subsemiring.toCommSemiring, @Subsemiring.commSemiring, @Subalgebra.toCommSemiring, @Subalgebra.instCommSemiringSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraCenter, @RingCon.instCommSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToMul, Int.instCommSemiringInt, instCommSemiringRestrictScalars, Nat.commSemiring, @Prod.instCommSemiring, @WithTop.commSemiring]
[Meta.synthInstance] [0.000023s] 💥 apply @WithTop.commSemiring to CommSemiring ?m.2142
[Meta.synthInstance.tryResolve] [0.000012s] 💥 CommSemiring ?m.2142 ≟ CommSemiring (WithTop ?m.2348)
[Meta.isDefEq] [0.000010s] 💥 CommSemiring ?m.2142 =?= CommSemiring (WithTop ?m.2348)
[Meta.isDefEq] [0.000001s] 💥 ?m.2142 =?= WithTop ?m.2348
[Meta.isDefEq] ?m.2142 [nonassignable] =?= WithTop ?m.2348 [nonassignable]
[Meta.isDefEq] [0.000002s] 💥 ?m.2143 =?= CommSemiring.toSemiring
[Meta.isDefEq] ?m.2143 [nonassignable] =?= CommSemiring.toSemiring [nonassignable]
[Meta.isDefEq] [0.000006s] ✅ R =?= ?m.2354
[Meta.isDefEq] R [nonassignable] =?= ?m.2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment