I have a really simple example that I can't get working, involving instantiatations with multiple type parameters:

```
datatype ('a, 'b) MyT = MyT 'b
instantiation MyT :: (_, plus) plus
begin
fun plus_MyT :: "('l, 'a::plus) MyT ⇒ ('l, 'a) MyT ⇒ ('l, 'a) MyT" where
"plus_MyT (MyT a) (MyT b) = MyT (a + b)"
instance ..
end
```

When I run this, I get an error on the constraint `'a::plus`

saying

```
Sort constraint plus inconsistent with default type for type variable "'a"⌂
```

So it looks like for the second type param, it's reading the constraint for the first param `_`

? Curiously, when I write

```
instantiation MyT :: (plus, _) plus
```

it _does_ compile, but note that this is obviously not what I want to do, because then I don't get an instance for, say, `(unit, nat) MyT`

:

```
value "MyT 5 + (MyT 6 :: (unit, nat) MyT)"
```

gives error:

```
Type unification failed: No type arity unit :: plus
```

I really don't understand why this second example is valid but the first one isn't

```
datatype ('a, 'b) MyT = MyT 'b
instantiation MyT :: (_, plus) plus
begin
fun plus_MyT :: "('a, 'b::plus) MyT ⇒ ('a, 'b) MyT ⇒ ('a, 'b) MyT" where
"plus_MyT (MyT a) (MyT b) = MyT (a + b)"
instance ..
end
```

the type unification gives the names 'a, 'b, and so on. So your `'l, 'a::plus`

does not work

gotcha. Huh. Interesting. Very quick response though appreciated

to be fair to my original example, of which this is an MWE, my actual type has something like

```
datatype ('l, 'a) MyT = MyT 'a
```

which is why I still had the 'l and 'a naming going on

Last updated: Dec 07 2023 at 08:19 UTC