Ayaz Hafiz (Jul 06 2023 at 18:35): Ayaz Hafiz (Jul 06 2023 at 18:35):From #beginners > Abilities with type variables - we need to tighten up the type-checking of ability impls against their prototype signatures.
Let's use <r>a to say a type variable is rigid, and <f>a to say it is flexible (resp. Content::FlexVar/Content::RigidVar in the implementation).
Given a prototype
ability Ab has
f : a -> b | a has Ab
we solve the type as
<r>a -> <r>b | a has Ab
The type checking should keep the variables as rigid in the prototype signature, instantiate rigid variables to flex variables in the implementation signature, and unify the signatures with a special-case of allowing any type to unify with the rigid variable that is the target of the ability specialization.
For example, with the following cases:
<r>c -> <r>dinstantiate impl type: <f>c -> <f>d
unify against prototype: <r>a -> r<b> | a has Ab ~ <f>c -> <f>d
solved type:
<f>c = <r>a | a has Ab
<f>d = <r>b
:check:
<r>c -> <r>cinstantiate impl type: <f>c -> <f>c
unify against prototype: <r>a -> r<b> | a has Ab ~ <f>c -> <f>c
solved type:
<f>c = <r>a | a has Ab
<f>c = <r>a = <r>b
:cross_mark: rigids can never be equal, this is a type error
<f>c -> <f>cinstantiate impl type: <f>c -> <f>c
unify against prototype: <r>a -> r<b> | a has Ab ~ <f>c -> <f>c
solved type:
<f>c = <r>a | a has Ab
<f>c = <r>a = <r>b
:cross_mark: rigids can never be equal, this is a type error
Foo -> <r>c, Foo is an opaque typeinstantiate impl type: Foo -> <f>c
unify against prototype: <r>a -> r<b> | a has Ab ~ <f>c -> <f>c
solved type:
Foo= <r>a | a has Ab <-- this is a needed new special case for ability checking
<f>c = <r>b
:check:
Filed https://github.com/roc-lang/roc/issues/5645
Richard Feldman (Jul 06 2023 at 19:52):nice, makes sense! :thumbs_up:
Last updated: Jul 06 2025 at 12:14 UTC