type check error (higher order unification?)

[Tao Yang]

Hi,

I run into a problem while trying to add type annotations to funcool/cats
<https://github.com/funcool/cats>. I started with two very basic things,
monoid and semigroup. There is a type error on this line of test
<https://github.com/kazuhiro/cats.typed/compare/master...taojang:semigrp-monoid?expand=1#diff-310f7584031fe976c61d2f632f676e70R23>

Type Error (cats/typed/core.clj:24:21)
Type mismatch:

Expected: (t/All [x] (t/Option (t/I Context (t/U (Semigroup x) (Monoid x
)))))

Actual: (t/I Context (Monoid t/Bool))


Type Error (cats/typed/core.clj:24:3)
Function cats.protocols/-get-level could not be applied to arguments:


Domains:
Context

Arguments:
(t/All [x] (t/Option (t/I Context (t/U (Monoid x) (Semigroup x)))))

Ranges:
t/Num


For me as someone with no exposure to type theory,
(I Context (Monoid Bool))
does not contradict to
(All [x] (Option (I Context (U (Monoid x) (Semigroup x)))))

However I think it's more likely that I've done something stupid. Any idea
please?

Thanks,
Tao

[Ambrose Bonnaire-Sergeant]

Hi Tao,

Unfortunately core.typed is currently bad at this kind of thing.

Try using a TFn instead of All here
<https://github.com/kazuhiro/cats.typed/compare/master...taojang:semigrp-monoid?expand=1#diff-eda93ec6c3800ab04c596f20c0e2ff58R7>,
and any other place that
isn't just defining a polymorphic function.

Thanks,
Ambrose

Post by Tao Yang
Hi,
I run into a problem while trying to add type annotations to funcool/cats
<https://github.com/funcool/cats>. I started with two very basic things,
monoid and semigroup. There is a type error on this line of test
<https://github.com/kazuhiro/cats.typed/compare/master...taojang:semigrp-monoid?expand=1#diff-310f7584031fe976c61d2f632f676e70R23>
Type Error (cats/typed/core.clj:24:21)
Expected: (t/All [x] (t/Option (t/I Context (t/U (Semigroup x) (Monoid
x)))))
Actual: (t/I Context (Monoid t/Bool))
Type Error (cats/typed/core.clj:24:3)
Context
(t/All [x] (t/Option (t/I Context (t/U (Monoid x) (Semigroup x)))))
t/Num
For me as someone with no exposure to type theory,
(I Context (Monoid Bool))
does not contradict to
(All [x] (Option (I Context (U (Monoid x) (Semigroup x)))))
However I think it's more likely that I've done something stupid. Any idea
please?
Thanks,
Tao