diff --git a/compiler/can/src/abilities.rs b/compiler/can/src/abilities.rs
index 43f958eece..d2aef3fbd2 100644
--- a/compiler/can/src/abilities.rs
+++ b/compiler/can/src/abilities.rs
@@ -6,6 +6,8 @@ use roc_types::{subs::Variable, types::Type};
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct MemberVariables {
     pub able_vars: Vec<Variable>,
+    /// This includes - named rigid vars, lambda sets, wildcards. See
+    /// [`IntroducedVariables::collect_rigid`](crate::annotation::IntroducedVariables::collect_rigid).
     pub rigid_vars: Vec<Variable>,
     pub flex_vars: Vec<Variable>,
 }
@@ -13,7 +15,7 @@ pub struct MemberVariables {
 /// Stores information about an ability member definition, including the parent ability, the
 /// defining type, and what type variables need to be instantiated with instances of the ability.
 // TODO: SoA and put me in an arena
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, Clone)]
 pub struct AbilityMemberData {
     pub parent_ability: Symbol,
     pub signature_var: Variable,
@@ -29,11 +31,22 @@ pub struct MemberSpecialization {
     pub region: Region,
 }
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct SpecializationId(u64);
+
+#[allow(clippy::derivable_impls)] // let's be explicit about this
+impl Default for SpecializationId {
+    fn default() -> Self {
+        Self(0)
+    }
+}
+
 /// Stores information about what abilities exist in a scope, what it means to implement an
 /// ability, and what types implement them.
 // TODO(abilities): this should probably go on the Scope, I don't put it there for now because we
-// are only dealing with inter-module abilities for now.
-#[derive(Default, Debug, Clone, PartialEq, Eq)]
+// are only dealing with intra-module abilities for now.
+// TODO(abilities): many of these should be `VecMap`s. Do some benchmarking.
+#[derive(Default, Debug, Clone)]
 pub struct AbilitiesStore {
     /// Maps an ability to the members defining it.
     members_of_ability: MutMap<Symbol, Vec<Symbol>>,
@@ -54,6 +67,12 @@ pub struct AbilitiesStore {
     /// Maps a tuple (member, type) specifying that `type` declares an implementation of an ability
     /// member `member`, to the exact symbol that implements the ability.
     declared_specializations: MutMap<(Symbol, Symbol), MemberSpecialization>,
+
+    next_specialization_id: u64,
+
+    /// Resolved specializations for a symbol. These might be ephemeral (known due to type solving),
+    /// or resolved on-the-fly during mono.
+    resolved_specializations: MutMap<SpecializationId, Symbol>,
 }
 
 impl AbilitiesStore {
@@ -168,4 +187,37 @@ impl AbilitiesStore {
     pub fn members_of_ability(&self, ability: Symbol) -> Option<&[Symbol]> {
         self.members_of_ability.get(&ability).map(|v| v.as_ref())
     }
+
+    pub fn fresh_specialization_id(&mut self) -> SpecializationId {
+        debug_assert!(self.next_specialization_id != std::u64::MAX);
+
+        let id = SpecializationId(self.next_specialization_id);
+        self.next_specialization_id += 1;
+        id
+    }
+
+    pub fn insert_resolved(&mut self, id: SpecializationId, specialization: Symbol) {
+        debug_assert!(self.is_specialization_name(specialization));
+
+        let old_specialization = self.resolved_specializations.insert(id, specialization);
+
+        debug_assert!(
+            old_specialization.is_none(),
+            "Existing resolution: {:?}",
+            old_specialization
+        );
+    }
+
+    pub fn remove_resolved(&mut self, id: SpecializationId) {
+        let old_specialization = self.resolved_specializations.remove(&id);
+
+        debug_assert!(
+            old_specialization.is_some(),
+            "Trying to remove a resolved specialization that was never there!",
+        );
+    }
+
+    pub fn get_resolved(&self, id: SpecializationId) -> Option<Symbol> {
+        self.resolved_specializations.get(&id).copied()
+    }
 }
diff --git a/compiler/can/src/annotation.rs b/compiler/can/src/annotation.rs
index 97cc04ee9a..0a567e12e7 100644
--- a/compiler/can/src/annotation.rs
+++ b/compiler/can/src/annotation.rs
@@ -9,8 +9,8 @@ use roc_problem::can::ShadowKind;
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{VarStore, Variable};
 use roc_types::types::{
-    name_type_var, Alias, AliasCommon, AliasKind, LambdaSet, Problem, RecordField, Type,
-    TypeExtension,
+    name_type_var, Alias, AliasCommon, AliasKind, AliasVar, LambdaSet, OptAbleType, OptAbleVar,
+    Problem, RecordField, Type, TypeExtension,
 };
 
 #[derive(Clone, Debug)]
@@ -71,6 +71,48 @@ impl<'a> NamedOrAbleVariable<'a> {
     }
 }
 
+pub enum OwnedNamedOrAble {
+    Named(NamedVariable),
+    Able(AbleVariable),
+}
+
+impl OwnedNamedOrAble {
+    pub fn first_seen(&self) -> Region {
+        match self {
+            OwnedNamedOrAble::Named(nv) => nv.first_seen,
+            OwnedNamedOrAble::Able(av) => av.first_seen,
+        }
+    }
+
+    pub fn ref_name(&self) -> &Lowercase {
+        match self {
+            OwnedNamedOrAble::Named(nv) => &nv.name,
+            OwnedNamedOrAble::Able(av) => &av.name,
+        }
+    }
+
+    pub fn name(self) -> Lowercase {
+        match self {
+            OwnedNamedOrAble::Named(nv) => nv.name,
+            OwnedNamedOrAble::Able(av) => av.name,
+        }
+    }
+
+    pub fn variable(&self) -> Variable {
+        match self {
+            OwnedNamedOrAble::Named(nv) => nv.variable,
+            OwnedNamedOrAble::Able(av) => av.variable,
+        }
+    }
+
+    pub fn opt_ability(&self) -> Option<Symbol> {
+        match self {
+            OwnedNamedOrAble::Named(_) => None,
+            OwnedNamedOrAble::Able(av) => Some(av.ability),
+        }
+    }
+}
+
 /// A named type variable, not bound to an ability.
 #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
 pub struct NamedVariable {
@@ -603,7 +645,7 @@ fn can_annotation_help(
                 references,
             );
             let mut vars = Vec::with_capacity(loc_vars.len());
-            let mut lowercase_vars = Vec::with_capacity(loc_vars.len());
+            let mut lowercase_vars: Vec<Loc<AliasVar>> = Vec::with_capacity(loc_vars.len());
 
             references.insert(symbol);
 
@@ -616,9 +658,17 @@ fn can_annotation_help(
                 };
                 let var_name = Lowercase::from(var);
 
+                // TODO(abilities): check that there are no abilities bound here.
                 if let Some(var) = introduced_variables.var_by_name(&var_name) {
                     vars.push(Type::Variable(var));
-                    lowercase_vars.push(Loc::at(loc_var.region, (var_name, var)));
+                    lowercase_vars.push(Loc::at(
+                        loc_var.region,
+                        AliasVar {
+                            name: var_name,
+                            var,
+                            opt_bound_ability: None,
+                        },
+                    ));
                 } else {
                     let var = var_store.fresh();
 
@@ -626,7 +676,14 @@ fn can_annotation_help(
                         .insert_named(var_name.clone(), Loc::at(loc_var.region, var));
                     vars.push(Type::Variable(var));
 
-                    lowercase_vars.push(Loc::at(loc_var.region, (var_name, var)));
+                    lowercase_vars.push(Loc::at(
+                        loc_var.region,
+                        AliasVar {
+                            name: var_name,
+                            var,
+                            opt_bound_ability: None,
+                        },
+                    ));
                 }
             }
 
@@ -675,7 +732,7 @@ fn can_annotation_help(
             hidden_variables.extend(alias_actual.variables());
 
             for loc_var in lowercase_vars.iter() {
-                hidden_variables.remove(&loc_var.value.1);
+                hidden_variables.remove(&loc_var.value.var);
             }
 
             scope.add_alias(
@@ -702,7 +759,13 @@ fn can_annotation_help(
             } else {
                 Type::Alias {
                     symbol,
-                    type_arguments: vars,
+                    type_arguments: vars
+                        .into_iter()
+                        .map(|typ| OptAbleType {
+                            typ,
+                            opt_ability: None,
+                        })
+                        .collect(),
                     lambda_set_variables: alias.lambda_set_variables.clone(),
                     actual: Box::new(alias.typ.clone()),
                     kind: alias.kind,
@@ -995,7 +1058,7 @@ fn shallow_dealias_with_scope<'a>(scope: &'a mut Scope, typ: &'a Type) -> &'a Ty
 pub fn instantiate_and_freshen_alias_type(
     var_store: &mut VarStore,
     introduced_variables: &mut IntroducedVariables,
-    type_variables: &[Loc<(Lowercase, Variable)>],
+    type_variables: &[Loc<AliasVar>],
     type_arguments: Vec<Type>,
     lambda_set_variables: &[LambdaSet],
     mut actual_type: Type,
@@ -1004,8 +1067,8 @@ pub fn instantiate_and_freshen_alias_type(
     let mut type_var_to_arg = Vec::new();
 
     for (loc_var, arg_ann) in type_variables.iter().zip(type_arguments.into_iter()) {
-        let name = loc_var.value.0.clone();
-        let var = loc_var.value.1;
+        let name = loc_var.value.name.clone();
+        let var = loc_var.value.var;
 
         substitutions.insert(var, arg_ann.clone());
         type_var_to_arg.push((name.clone(), arg_ann));
@@ -1040,19 +1103,21 @@ pub fn instantiate_and_freshen_alias_type(
 pub fn freshen_opaque_def(
     var_store: &mut VarStore,
     opaque: &Alias,
-) -> (Vec<Variable>, Vec<LambdaSet>, Type) {
+) -> (Vec<OptAbleVar>, Vec<LambdaSet>, Type) {
     debug_assert!(opaque.kind == AliasKind::Opaque);
 
-    let fresh_variables: Vec<Variable> = opaque
+    let fresh_variables: Vec<OptAbleVar> = opaque
         .type_variables
         .iter()
-        .map(|_| var_store.fresh())
+        .map(|alias_var| OptAbleVar {
+            var: var_store.fresh(),
+            opt_ability: alias_var.value.opt_bound_ability,
+        })
         .collect();
 
     let fresh_type_arguments = fresh_variables
         .iter()
-        .copied()
-        .map(Type::Variable)
+        .map(|av| Type::Variable(av.var))
         .collect();
 
     // NB: We don't introduce the fresh variables here, we introduce them during constraint gen.
diff --git a/compiler/can/src/def.rs b/compiler/can/src/def.rs
index 0dd250fef9..ed4c1dc2a0 100644
--- a/compiler/can/src/def.rs
+++ b/compiler/can/src/def.rs
@@ -2,6 +2,7 @@ use crate::abilities::MemberVariables;
 use crate::annotation::canonicalize_annotation;
 use crate::annotation::find_type_def_symbols;
 use crate::annotation::IntroducedVariables;
+use crate::annotation::OwnedNamedOrAble;
 use crate::env::Env;
 use crate::expr::AnnotatedMark;
 use crate::expr::ClosureData;
@@ -29,6 +30,7 @@ use roc_problem::can::{CycleEntry, Problem, RuntimeError};
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{VarStore, Variable};
 use roc_types::types::AliasKind;
+use roc_types::types::AliasVar;
 use roc_types::types::LambdaSet;
 use roc_types::types::{Alias, Type};
 use std::fmt::Debug;
@@ -318,38 +320,43 @@ pub(crate) fn canonicalize_defs<'a>(
                     &abilities_in_scope,
                 );
 
-                // Does this alias reference any abilities? For now, we don't permit that.
-                let ability_references = can_ann
-                    .references
-                    .iter()
-                    .filter_map(|&ty_ref| abilities_in_scope.iter().find(|&&name| name == ty_ref))
-                    .collect::<Vec<_>>();
-
-                if let Some(one_ability_ref) = ability_references.first() {
-                    env.problem(Problem::AliasUsesAbility {
-                        loc_name: name,
-                        ability: **one_ability_ref,
-                    });
-                }
-
                 // Record all the annotation's references in output.references.lookups
                 for symbol in can_ann.references {
                     output.references.insert_type_lookup(symbol);
                 }
 
-                let mut can_vars: Vec<Loc<(Lowercase, Variable)>> = Vec::with_capacity(vars.len());
+                let mut can_vars: Vec<Loc<AliasVar>> = Vec::with_capacity(vars.len());
                 let mut is_phantom = false;
 
-                let mut named = can_ann.introduced_variables.named;
+                let IntroducedVariables {
+                    named,
+                    able,
+                    wildcards,
+                    inferred,
+                    ..
+                } = can_ann.introduced_variables;
+
+                let mut named: Vec<_> = (named.into_iter().map(OwnedNamedOrAble::Named))
+                    .chain(able.into_iter().map(OwnedNamedOrAble::Able))
+                    .collect();
                 for loc_lowercase in vars.iter() {
-                    let opt_index = named.iter().position(|nv| nv.name == loc_lowercase.value);
+                    let opt_index = named
+                        .iter()
+                        .position(|nv| nv.ref_name() == &loc_lowercase.value);
                     match opt_index {
                         Some(index) => {
                             // This is a valid lowercase rigid var for the type def.
                             let named_variable = named.swap_remove(index);
+                            let var = named_variable.variable();
+                            let opt_bound_ability = named_variable.opt_ability();
+                            let name = named_variable.name();
 
                             can_vars.push(Loc {
-                                value: (named_variable.name, named_variable.variable),
+                                value: AliasVar {
+                                    name,
+                                    var,
+                                    opt_bound_ability,
+                                },
                                 region: loc_lowercase.region,
                             });
                         }
@@ -370,16 +377,11 @@ pub(crate) fn canonicalize_defs<'a>(
                     continue;
                 }
 
-                let IntroducedVariables {
-                    wildcards,
-                    inferred,
-                    ..
-                } = can_ann.introduced_variables;
                 let num_unbound = named.len() + wildcards.len() + inferred.len();
                 if num_unbound > 0 {
                     let one_occurrence = named
                         .iter()
-                        .map(|nv| Loc::at(nv.first_seen, nv.variable))
+                        .map(|nv| Loc::at(nv.first_seen(), nv.variable()))
                         .chain(wildcards)
                         .chain(inferred)
                         .next()
@@ -578,12 +580,14 @@ fn resolve_abilities<'a>(
 
             // What variables in the annotation are bound to the parent ability, and what variables
             // are bound to some other ability?
-            let (variables_bound_to_ability, variables_bound_to_other_abilities): (Vec<_>, Vec<_>) =
-                member_annot
-                    .introduced_variables
-                    .able
-                    .iter()
-                    .partition(|av| av.ability == loc_ability_name.value);
+            let (variables_bound_to_ability, _variables_bound_to_other_abilities): (
+                Vec<_>,
+                Vec<_>,
+            ) = member_annot
+                .introduced_variables
+                .able
+                .iter()
+                .partition(|av| av.ability == loc_ability_name.value);
 
             let mut bad_has_clauses = false;
 
@@ -618,18 +622,6 @@ fn resolve_abilities<'a>(
                 bad_has_clauses = true;
             }
 
-            if !variables_bound_to_other_abilities.is_empty() {
-                // Disallow variables bound to other abilities, for now.
-                for bad_variable in variables_bound_to_other_abilities.iter() {
-                    env.problem(Problem::AbilityMemberBindsExternalAbility {
-                        member: member_sym,
-                        ability: loc_ability_name.value,
-                        region: bad_variable.first_seen,
-                    });
-                }
-                bad_has_clauses = true;
-            }
-
             if bad_has_clauses {
                 // Pretend the member isn't a part of the ability
                 continue;
@@ -1740,7 +1732,7 @@ fn make_tag_union_of_alias_recursive<'a>(
     let alias_args = alias
         .type_variables
         .iter()
-        .map(|l| (l.value.0.clone(), Type::Variable(l.value.1)))
+        .map(|l| (l.value.name.clone(), Type::Variable(l.value.var)))
         .collect::<Vec<_>>();
 
     let made_recursive = make_tag_union_recursive_help(
@@ -1847,10 +1839,17 @@ fn make_tag_union_recursive_help<'a, 'b>(
             type_arguments,
             ..
         } => {
+            // NB: We need to collect the type arguments to shut off rustc's closure type
+            // instantiator. Otherwise we get unfortunate errors like
+            //   reached the recursion limit while instantiating `make_tag_union_recursive_help::<...n/src/def.rs:1879:65: 1879:77]>>`
+            #[allow(clippy::needless_collect)]
+            let type_arguments: Vec<&Type> = type_arguments.iter().map(|ta| &ta.typ).collect();
+            let recursive_alias = Loc::at_zero((symbol, type_arguments.into_iter()));
+
             // try to make `actual` recursive
             make_tag_union_recursive_help(
                 env,
-                Loc::at_zero((symbol, type_arguments.iter())),
+                recursive_alias,
                 region,
                 others,
                 actual,
diff --git a/compiler/can/src/effect_module.rs b/compiler/can/src/effect_module.rs
index 606fcbdfa0..7e055f3126 100644
--- a/compiler/can/src/effect_module.rs
+++ b/compiler/can/src/effect_module.rs
@@ -9,7 +9,7 @@ use roc_module::ident::TagName;
 use roc_module::symbol::Symbol;
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{ExhaustiveMark, RedundantMark, VarStore, Variable};
-use roc_types::types::{AliasKind, LambdaSet, Type, TypeExtension};
+use roc_types::types::{AliasKind, LambdaSet, OptAbleType, OptAbleVar, Type, TypeExtension};
 
 #[derive(Debug, Default, Clone, Copy)]
 pub(crate) struct HostedGeneratedFunctions {
@@ -1007,7 +1007,7 @@ fn build_effect_loop(
 
             Type::Alias {
                 symbol: effect_symbol,
-                type_arguments: vec![state_type],
+                type_arguments: vec![OptAbleType::unbound(state_type)],
                 lambda_set_variables: vec![roc_types::types::LambdaSet(Type::Variable(
                     closure_var,
                 ))],
@@ -1445,7 +1445,7 @@ fn build_effect_opaque(
 
     Type::Alias {
         symbol: effect_symbol,
-        type_arguments: vec![Type::Variable(a_var)],
+        type_arguments: vec![OptAbleType::unbound(Type::Variable(a_var))],
         lambda_set_variables: vec![roc_types::types::LambdaSet(Type::Variable(closure_var))],
         actual: Box::new(actual),
         kind: AliasKind::Opaque,
@@ -1454,7 +1454,7 @@ fn build_effect_opaque(
 
 fn build_fresh_opaque_variables(
     var_store: &mut VarStore,
-) -> (Box<Type>, Vec<Variable>, Vec<LambdaSet>) {
+) -> (Box<Type>, Vec<OptAbleVar>, Vec<LambdaSet>) {
     let closure_var = var_store.fresh();
 
     // NB: if there are bugs, check whether not introducing variables is a problem!
@@ -1466,7 +1466,10 @@ fn build_fresh_opaque_variables(
         Box::new(Type::Variable(closure_var)),
         Box::new(Type::Variable(a_var)),
     );
-    let type_arguments = vec![a_var];
+    let type_arguments = vec![OptAbleVar {
+        var: a_var,
+        opt_ability: None,
+    }];
     let lambda_set_variables = vec![roc_types::types::LambdaSet(Type::Variable(closure_var))];
 
     (Box::new(actual), type_arguments, lambda_set_variables)
diff --git a/compiler/can/src/expr.rs b/compiler/can/src/expr.rs
index 132def6f42..3b6c99898a 100644
--- a/compiler/can/src/expr.rs
+++ b/compiler/can/src/expr.rs
@@ -1,3 +1,4 @@
+use crate::abilities::SpecializationId;
 use crate::annotation::{freshen_opaque_def, IntroducedVariables};
 use crate::builtins::builtin_defs_map;
 use crate::def::{can_defs_with_return, Def};
@@ -19,7 +20,7 @@ use roc_parse::pattern::PatternType::*;
 use roc_problem::can::{PrecedenceProblem, Problem, RuntimeError};
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{ExhaustiveMark, RedundantMark, VarStore, Variable};
-use roc_types::types::{Alias, Category, LambdaSet, Type};
+use roc_types::types::{Alias, Category, LambdaSet, OptAbleVar, Type};
 use std::fmt::{Debug, Display};
 use std::{char, u32};
 
@@ -83,6 +84,13 @@ pub enum Expr {
 
     // Lookups
     Var(Symbol),
+    AbilityMember(
+        /// Actual member name
+        Symbol,
+        /// Specialization to use
+        SpecializationId,
+    ),
+
     // Branching
     When {
         /// The actual condition of the when expression.
@@ -191,7 +199,7 @@ pub enum Expr {
         // for the expression from the opaque definition. `type_arguments` is something like
         // [(n, fresh1)], and `specialized_def_type` becomes "[ Id U64 fresh1 ]".
         specialized_def_type: Box<Type>,
-        type_arguments: Vec<Variable>,
+        type_arguments: Vec<OptAbleVar>,
         lambda_set_variables: Vec<LambdaSet>,
     },
 
@@ -212,6 +220,7 @@ impl Expr {
             Self::SingleQuote(..) => Category::Character,
             Self::List { .. } => Category::List,
             &Self::Var(sym) => Category::Lookup(sym),
+            &Self::AbilityMember(sym, _) => Category::Lookup(sym),
             Self::When { .. } => Category::When,
             Self::If { .. } => Category::If,
             Self::LetRec(_, expr) => expr.value.category(),
@@ -390,6 +399,17 @@ impl WhenBranch {
     }
 }
 
+impl WhenBranch {
+    pub fn region(&self) -> Region {
+        Region::across_all(
+            self.patterns
+                .iter()
+                .map(|p| &p.region)
+                .chain([self.value.region].iter()),
+        )
+    }
+}
+
 pub fn canonicalize_expr<'a>(
     env: &mut Env<'a>,
     var_store: &mut VarStore,
@@ -1307,7 +1327,11 @@ fn canonicalize_var_lookup(
             Ok(symbol) => {
                 output.references.insert_value_lookup(symbol);
 
-                Var(symbol)
+                if scope.abilities_store.is_ability_member_name(symbol) {
+                    AbilityMember(symbol, scope.abilities_store.fresh_specialization_id())
+                } else {
+                    Var(symbol)
+                }
             }
             Err(problem) => {
                 env.problem(Problem::RuntimeError(problem.clone()));
@@ -1322,7 +1346,11 @@ fn canonicalize_var_lookup(
             Ok(symbol) => {
                 output.references.insert_value_lookup(symbol);
 
-                Var(symbol)
+                if scope.abilities_store.is_ability_member_name(symbol) {
+                    AbilityMember(symbol, scope.abilities_store.fresh_specialization_id())
+                } else {
+                    Var(symbol)
+                }
             }
             Err(problem) => {
                 // Either the module wasn't imported, or
@@ -1356,6 +1384,7 @@ pub fn inline_calls(var_store: &mut VarStore, scope: &mut Scope, expr: Expr) ->
         | other @ Accessor { .. }
         | other @ Update { .. }
         | other @ Var(_)
+        | other @ AbilityMember(..)
         | other @ RunLowLevel { .. }
         | other @ ForeignCall { .. } => other,
 
diff --git a/compiler/can/src/module.rs b/compiler/can/src/module.rs
index 5d90542d58..2d0fda6c9b 100644
--- a/compiler/can/src/module.rs
+++ b/compiler/can/src/module.rs
@@ -18,7 +18,7 @@ use roc_parse::pattern::PatternType;
 use roc_problem::can::{Problem, RuntimeError};
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{VarStore, Variable};
-use roc_types::types::{Alias, AliasKind, Type};
+use roc_types::types::{Alias, AliasKind, AliasVar, Type};
 
 #[derive(Debug)]
 pub struct Module {
@@ -119,7 +119,7 @@ impl GeneratedInfo {
                     scope.add_alias(
                         effect_symbol,
                         Region::zero(),
-                        vec![Loc::at_zero(("a".into(), a_var))],
+                        vec![Loc::at_zero(AliasVar::unbound("a".into(), a_var))],
                         actual,
                         AliasKind::Opaque,
                     );
@@ -704,6 +704,7 @@ fn fix_values_captured_in_closure_expr(
         | Str(_)
         | SingleQuote(_)
         | Var(_)
+        | AbilityMember(..)
         | EmptyRecord
         | RuntimeError(_)
         | ZeroArgumentTag { .. }
diff --git a/compiler/can/src/pattern.rs b/compiler/can/src/pattern.rs
index db26136195..e06f695b29 100644
--- a/compiler/can/src/pattern.rs
+++ b/compiler/can/src/pattern.rs
@@ -13,7 +13,7 @@ use roc_parse::pattern::PatternType;
 use roc_problem::can::{MalformedPatternProblem, Problem, RuntimeError, ShadowKind};
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{VarStore, Variable};
-use roc_types::types::{LambdaSet, PatternCategory, Type};
+use roc_types::types::{LambdaSet, OptAbleVar, PatternCategory, Type};
 
 /// A pattern, including possible problems (e.g. shadowing) so that
 /// codegen can generate a runtime error if this pattern is reached.
@@ -47,7 +47,7 @@ pub enum Pattern {
         // for the expression from the opaque definition. `type_arguments` is something like
         // [(n, fresh1)], and `specialized_def_type` becomes "[ Id U64 fresh1 ]".
         specialized_def_type: Box<Type>,
-        type_arguments: Vec<Variable>,
+        type_arguments: Vec<OptAbleVar>,
         lambda_set_variables: Vec<LambdaSet>,
     },
     RecordDestructure {
diff --git a/compiler/can/src/scope.rs b/compiler/can/src/scope.rs
index 860cf04904..52867942b8 100644
--- a/compiler/can/src/scope.rs
+++ b/compiler/can/src/scope.rs
@@ -1,10 +1,9 @@
 use roc_collections::VecMap;
-use roc_module::ident::{Ident, Lowercase};
+use roc_module::ident::Ident;
 use roc_module::symbol::{IdentId, IdentIds, ModuleId, Symbol};
 use roc_problem::can::RuntimeError;
 use roc_region::all::{Loc, Region};
-use roc_types::subs::Variable;
-use roc_types::types::{Alias, AliasKind, Type};
+use roc_types::types::{Alias, AliasKind, AliasVar, Type};
 
 use crate::abilities::AbilitiesStore;
 
@@ -335,7 +334,7 @@ impl Scope {
         &mut self,
         name: Symbol,
         region: Region,
-        vars: Vec<Loc<(Lowercase, Variable)>>,
+        vars: Vec<Loc<AliasVar>>,
         typ: Type,
         kind: AliasKind,
     ) {
@@ -394,7 +393,7 @@ impl Scope {
 pub fn create_alias(
     name: Symbol,
     region: Region,
-    vars: Vec<Loc<(Lowercase, Variable)>>,
+    vars: Vec<Loc<AliasVar>>,
     typ: Type,
     kind: AliasKind,
 ) -> Alias {
@@ -408,7 +407,7 @@ pub fn create_alias(
         let mut hidden = type_variables;
 
         for loc_var in vars.iter() {
-            hidden.remove(&loc_var.value.1);
+            hidden.remove(&loc_var.value.var);
         }
 
         if !hidden.is_empty() {
diff --git a/compiler/can/src/traverse.rs b/compiler/can/src/traverse.rs
index 55ecdf14b9..7a23cdf20f 100644
--- a/compiler/can/src/traverse.rs
+++ b/compiler/can/src/traverse.rs
@@ -1,11 +1,12 @@
 //! Traversals over the can ast.
 
+use roc_module::ident::Lowercase;
 use roc_region::all::{Loc, Region};
 use roc_types::subs::Variable;
 
 use crate::{
     def::{Annotation, Declaration, Def},
-    expr::{ClosureData, Expr, WhenBranch},
+    expr::{AccessorData, ClosureData, Expr, Field, WhenBranch},
     pattern::Pattern,
 };
 
@@ -17,11 +18,11 @@ macro_rules! visit_list {
     };
 }
 
-fn walk_decls<V: Visitor>(visitor: &mut V, decls: &[Declaration]) {
+pub fn walk_decls<V: Visitor>(visitor: &mut V, decls: &[Declaration]) {
     visit_list!(visitor, visit_decl, decls)
 }
 
-fn walk_decl<V: Visitor>(visitor: &mut V, decl: &Declaration) {
+pub fn walk_decl<V: Visitor>(visitor: &mut V, decl: &Declaration) {
     match decl {
         Declaration::Declare(def) => {
             visitor.visit_def(def);
@@ -31,12 +32,12 @@ fn walk_decl<V: Visitor>(visitor: &mut V, decl: &Declaration) {
         }
         Declaration::Builtin(def) => visitor.visit_def(def),
         Declaration::InvalidCycle(_cycles) => {
-            todo!()
+            // ignore
         }
     }
 }
 
-fn walk_def<V: Visitor>(visitor: &mut V, def: &Def) {
+pub fn walk_def<V: Visitor>(visitor: &mut V, def: &Def) {
     let Def {
         loc_pattern,
         loc_expr,
@@ -45,18 +46,19 @@ fn walk_def<V: Visitor>(visitor: &mut V, def: &Def) {
         ..
     } = def;
 
-    visitor.visit_pattern(
-        &loc_pattern.value,
-        loc_pattern.region,
-        loc_pattern.value.opt_var(),
-    );
+    let opt_var = match loc_pattern.value {
+        Pattern::Identifier(..) | Pattern::AbilityMemberSpecialization { .. } => Some(*expr_var),
+        _ => loc_pattern.value.opt_var(),
+    };
+
+    visitor.visit_pattern(&loc_pattern.value, loc_pattern.region, opt_var);
     visitor.visit_expr(&loc_expr.value, loc_expr.region, *expr_var);
     if let Some(annot) = &annotation {
         visitor.visit_annotation(annot);
     }
 }
 
-fn walk_expr<V: Visitor>(visitor: &mut V, expr: &Expr) {
+pub fn walk_expr<V: Visitor>(visitor: &mut V, expr: &Expr, var: Variable) {
     match expr {
         Expr::Closure(closure_data) => walk_closure(visitor, closure_data),
         Expr::When {
@@ -70,11 +72,107 @@ fn walk_expr<V: Visitor>(visitor: &mut V, expr: &Expr) {
         } => {
             walk_when(visitor, *cond_var, *expr_var, loc_cond, branches);
         }
-        e => todo!("{:?}", e),
+        Expr::Num(..) => { /* terminal */ }
+        Expr::Int(..) => { /* terminal */ }
+        Expr::Float(..) => { /* terminal */ }
+        Expr::Str(..) => { /* terminal */ }
+        Expr::SingleQuote(..) => { /* terminal */ }
+        Expr::List {
+            elem_var,
+            loc_elems,
+        } => {
+            walk_list(visitor, *elem_var, loc_elems);
+        }
+        Expr::Var(..) => { /* terminal */ }
+        Expr::AbilityMember(..) => { /* terminal */ }
+        Expr::If {
+            cond_var,
+            branches,
+            branch_var,
+            final_else,
+        } => walk_if(visitor, *cond_var, branches, *branch_var, final_else),
+        Expr::LetRec(defs, body) => {
+            defs.iter().for_each(|def| visitor.visit_def(def));
+            visitor.visit_expr(&body.value, body.region, var);
+        }
+        Expr::LetNonRec(def, body) => {
+            visitor.visit_def(def);
+            visitor.visit_expr(&body.value, body.region, var);
+        }
+        Expr::Call(f, args, _called_via) => {
+            let (fn_var, loc_fn, _closure_var, _ret_var) = &**f;
+            walk_call(visitor, *fn_var, loc_fn, args);
+        }
+        Expr::RunLowLevel {
+            op: _,
+            args,
+            ret_var: _,
+        } => {
+            args.iter()
+                .for_each(|(v, e)| visitor.visit_expr(e, Region::zero(), *v));
+        }
+        Expr::ForeignCall {
+            foreign_symbol: _,
+            args,
+            ret_var: _,
+        } => {
+            args.iter()
+                .for_each(|(v, e)| visitor.visit_expr(e, Region::zero(), *v));
+        }
+        Expr::Record {
+            record_var: _,
+            fields,
+        } => {
+            walk_record_fields(visitor, fields.iter());
+        }
+        Expr::EmptyRecord => { /* terminal */ }
+        Expr::Access {
+            field_var,
+            loc_expr,
+            field: _,
+            record_var: _,
+            ext_var: _,
+        } => visitor.visit_expr(&loc_expr.value, loc_expr.region, *field_var),
+        Expr::Accessor(AccessorData { .. }) => { /* terminal */ }
+        Expr::Update {
+            record_var: _,
+            ext_var: _,
+            symbol: _,
+            updates,
+        } => {
+            walk_record_fields(visitor, updates.iter());
+        }
+        Expr::Tag {
+            variant_var: _,
+            ext_var: _,
+            name: _,
+            arguments,
+        } => arguments
+            .iter()
+            .for_each(|(v, le)| visitor.visit_expr(&le.value, le.region, *v)),
+        Expr::ZeroArgumentTag { .. } => { /* terminal */ }
+        Expr::OpaqueRef {
+            opaque_var: _,
+            name: _,
+            argument,
+            specialized_def_type: _,
+            type_arguments: _,
+            lambda_set_variables: _,
+        } => {
+            let (var, le) = &**argument;
+            visitor.visit_expr(&le.value, le.region, *var);
+        }
+        Expr::Expect(e1, e2) => {
+            // TODO: what type does an expect have?
+            visitor.visit_expr(&e1.value, e1.region, Variable::NULL);
+            visitor.visit_expr(&e2.value, e2.region, Variable::NULL);
+        }
+        Expr::RuntimeError(..) => { /* terminal */ }
     }
 }
 
-fn walk_closure<V: Visitor>(visitor: &mut V, clos: &ClosureData) {
+#[inline(always)]
+pub fn walk_closure<V: Visitor>(visitor: &mut V, clos: &ClosureData) {
     let ClosureData {
         arguments,
         loc_body,
@@ -89,7 +187,8 @@ fn walk_closure<V: Visitor>(visitor: &mut V, clos: &ClosureData) {
     visitor.visit_expr(&loc_body.value, loc_body.region, *return_type);
 }
 
-fn walk_when<V: Visitor>(
+#[inline(always)]
+pub fn walk_when<V: Visitor>(
     visitor: &mut V,
     cond_var: Variable,
     expr_var: Variable,
@@ -103,7 +202,8 @@ fn walk_when<V: Visitor>(
         .for_each(|branch| walk_when_branch(visitor, branch, expr_var));
 }
 
-fn walk_when_branch<V: Visitor>(visitor: &mut V, branch: &WhenBranch, expr_var: Variable) {
+#[inline(always)]
+pub fn walk_when_branch<V: Visitor>(visitor: &mut V, branch: &WhenBranch, expr_var: Variable) {
     let WhenBranch {
         patterns,
         value,
@@ -120,11 +220,58 @@ fn walk_when_branch<V: Visitor>(visitor: &mut V, branch: &WhenBranch, expr_var:
     }
 }
 
-fn walk_pattern<V: Visitor>(_visitor: &mut V, _pat: &Pattern) {
-    todo!()
+#[inline(always)]
+pub fn walk_list<V: Visitor>(visitor: &mut V, elem_var: Variable, loc_elems: &[Loc<Expr>]) {
+    loc_elems
+        .iter()
+        .for_each(|le| visitor.visit_expr(&le.value, le.region, elem_var));
 }
 
-trait Visitor: Sized {
+#[inline(always)]
+pub fn walk_if<V: Visitor>(
+    visitor: &mut V,
+    cond_var: Variable,
+    branches: &[(Loc<Expr>, Loc<Expr>)],
+    branch_var: Variable,
+    final_else: &Loc<Expr>,
+) {
+    branches.iter().for_each(|(cond, body)| {
+        visitor.visit_expr(&cond.value, cond.region, cond_var);
+        visitor.visit_expr(&body.value, body.region, branch_var);
+    });
+    visitor.visit_expr(&final_else.value, final_else.region, branch_var);
+}
+
+#[inline(always)]
+pub fn walk_call<V: Visitor>(
+    visitor: &mut V,
+    fn_var: Variable,
+    fn_expr: &Loc<Expr>,
+    args: &[(Variable, Loc<Expr>)],
+) {
+    visitor.visit_expr(&fn_expr.value, fn_expr.region, fn_var);
+    args.iter()
+        .for_each(|(v, le)| visitor.visit_expr(&le.value, le.region, *v));
+}
+
+#[inline(always)]
+pub fn walk_record_fields<'a, V: Visitor>(
+    visitor: &mut V,
+    fields: impl Iterator<Item = (&'a Lowercase, &'a Field)>,
+) {
+    fields.for_each(
+        |(
+            _name,
+            Field {
+                var,
+                loc_expr,
+                region: _,
+            },
+        )| { visitor.visit_expr(&loc_expr.value, loc_expr.region, *var) },
+    )
+}
+
+pub trait Visitor: Sized + PatternVisitor {
     fn visit_decls(&mut self, decls: &[Declaration]) {
         walk_decls(self, decls);
     }
@@ -137,16 +284,22 @@ trait Visitor: Sized {
         walk_def(self, def);
     }
 
-    fn visit_pattern(&mut self, pat: &Pattern, _region: Region, _opt_var: Option<Variable>) {
-        walk_pattern(self, pat)
-    }
-
     fn visit_annotation(&mut self, _pat: &Annotation) {
-        // TODO
+        // ignore by default
     }
 
-    fn visit_expr(&mut self, expr: &Expr, _region: Region, _var: Variable) {
-        walk_expr(self, expr);
+    fn visit_expr(&mut self, expr: &Expr, _region: Region, var: Variable) {
+        walk_expr(self, expr, var);
+    }
+}
+
+pub fn walk_pattern<V: PatternVisitor>(_visitor: &mut V, _pattern: &Pattern) {
+    // ignore for now
+}
+
+pub trait PatternVisitor: Sized {
+    fn visit_pattern(&mut self, pattern: &Pattern, _region: Region, _opt_var: Option<Variable>) {
+        walk_pattern(self, pattern);
     }
 }
 
@@ -155,18 +308,7 @@ struct TypeAtVisitor {
     typ: Option<Variable>,
 }
 
-impl Visitor for TypeAtVisitor {
-    fn visit_expr(&mut self, expr: &Expr, region: Region, var: Variable) {
-        if region == self.region {
-            debug_assert!(self.typ.is_none());
-            self.typ = Some(var);
-            return;
-        }
-        if region.contains(&self.region) {
-            walk_expr(self, expr);
-        }
-    }
-
+impl PatternVisitor for TypeAtVisitor {
     fn visit_pattern(&mut self, pat: &Pattern, region: Region, opt_var: Option<Variable>) {
         if region == self.region {
             debug_assert!(self.typ.is_none());
@@ -178,6 +320,18 @@ impl Visitor for TypeAtVisitor {
         }
     }
 }
+impl Visitor for TypeAtVisitor {
+    fn visit_expr(&mut self, expr: &Expr, region: Region, var: Variable) {
+        if region == self.region {
+            debug_assert!(self.typ.is_none());
+            self.typ = Some(var);
+            return;
+        }
+        if region.contains(&self.region) {
+            walk_expr(self, expr, var);
+        }
+    }
+}
 
 /// Attempts to find the type of an expression at `region`, if it exists.
 pub fn find_type_at(region: Region, decls: &[Declaration]) -> Option<Variable> {
diff --git a/compiler/can/tests/helpers/mod.rs b/compiler/can/tests/helpers/mod.rs
index aaff51324c..038ae2cef1 100644
--- a/compiler/can/tests/helpers/mod.rs
+++ b/compiler/can/tests/helpers/mod.rs
@@ -11,7 +11,7 @@ use roc_module::symbol::{IdentIds, Interns, ModuleId, ModuleIds, Symbol};
 use roc_problem::can::Problem;
 use roc_region::all::{Loc, Region};
 use roc_types::subs::{VarStore, Variable};
-use roc_types::types::Type;
+use roc_types::types::{AliasVar, Type};
 use std::hash::Hash;
 
 pub fn test_home() -> ModuleId {
@@ -59,7 +59,10 @@ pub fn can_expr_with(arena: &Bump, home: ModuleId, expr_str: &str) -> CanExprOut
     scope.add_alias(
         Symbol::NUM_INT,
         Region::zero(),
-        vec![Loc::at_zero(("a".into(), Variable::EMPTY_RECORD))],
+        vec![Loc::at_zero(AliasVar::unbound(
+            "a".into(),
+            Variable::EMPTY_RECORD,
+        ))],
         Type::EmptyRec,
         roc_types::types::AliasKind::Structural,
     );
diff --git a/compiler/constrain/src/builtins.rs b/compiler/constrain/src/builtins.rs
index 7a0e9a73b3..a8095a825c 100644
--- a/compiler/constrain/src/builtins.rs
+++ b/compiler/constrain/src/builtins.rs
@@ -5,9 +5,9 @@ use roc_can::num::{FloatBound, FloatWidth, IntBound, IntWidth, NumericBound, Sig
 use roc_module::symbol::Symbol;
 use roc_region::all::Region;
 use roc_types::subs::Variable;
-use roc_types::types::Reason;
 use roc_types::types::Type::{self, *};
 use roc_types::types::{AliasKind, Category};
+use roc_types::types::{OptAbleType, Reason};
 
 #[must_use]
 #[inline(always)]
@@ -160,7 +160,7 @@ pub fn str_type() -> Type {
 #[inline(always)]
 fn builtin_alias(
     symbol: Symbol,
-    type_arguments: Vec<Type>,
+    type_arguments: Vec<OptAbleType>,
     actual: Box<Type>,
     kind: AliasKind,
 ) -> Type {
@@ -177,7 +177,7 @@ fn builtin_alias(
 pub fn num_float(range: Type) -> Type {
     builtin_alias(
         Symbol::NUM_FLOAT,
-        vec![range.clone()],
+        vec![OptAbleType::unbound(range.clone())],
         Box::new(num_num(num_floatingpoint(range))),
         AliasKind::Structural,
     )
@@ -187,7 +187,7 @@ pub fn num_float(range: Type) -> Type {
 pub fn num_floatingpoint(range: Type) -> Type {
     builtin_alias(
         Symbol::NUM_FLOATINGPOINT,
-        vec![range.clone()],
+        vec![OptAbleType::unbound(range.clone())],
         Box::new(range),
         AliasKind::Opaque,
     )
@@ -227,7 +227,7 @@ pub fn num_binary64() -> Type {
 pub fn num_int(range: Type) -> Type {
     builtin_alias(
         Symbol::NUM_INT,
-        vec![range.clone()],
+        vec![OptAbleType::unbound(range.clone())],
         Box::new(num_num(num_integer(range))),
         AliasKind::Structural,
     )
@@ -247,7 +247,7 @@ pub fn num_signed64() -> Type {
 pub fn num_integer(range: Type) -> Type {
     builtin_alias(
         Symbol::NUM_INTEGER,
-        vec![range.clone()],
+        vec![OptAbleType::unbound(range.clone())],
         Box::new(range),
         AliasKind::Opaque,
     )
@@ -257,7 +257,7 @@ pub fn num_integer(range: Type) -> Type {
 pub fn num_num(typ: Type) -> Type {
     builtin_alias(
         Symbol::NUM_NUM,
-        vec![typ.clone()],
+        vec![OptAbleType::unbound(typ.clone())],
         Box::new(typ),
         AliasKind::Opaque,
     )
diff --git a/compiler/constrain/src/expr.rs b/compiler/constrain/src/expr.rs
index a212adb654..d6dd14f57e 100644
--- a/compiler/constrain/src/expr.rs
+++ b/compiler/constrain/src/expr.rs
@@ -18,7 +18,7 @@ use roc_region::all::{Loc, Region};
 use roc_types::subs::Variable;
 use roc_types::types::Type::{self, *};
 use roc_types::types::{
-    AliasKind, AnnotationSource, Category, PReason, Reason, RecordField, TypeExtension,
+    AliasKind, AnnotationSource, Category, OptAbleType, PReason, Reason, RecordField, TypeExtension,
 };
 
 /// This is for constraining Defs
@@ -258,7 +258,7 @@ pub fn constrain_expr(
             let (fn_var, loc_fn, closure_var, ret_var) = &**boxed;
             // The expression that evaluates to the function being called, e.g. `foo` in
             // (foo) bar baz
-            let opt_symbol = if let Var(symbol) = loc_fn.value {
+            let opt_symbol = if let Var(symbol) | AbilityMember(symbol, _) = loc_fn.value {
                 Some(symbol)
             } else {
                 None
@@ -336,6 +336,11 @@ pub fn constrain_expr(
             // make lookup constraint to lookup this symbol's type in the environment
             constraints.lookup(*symbol, expected, region)
         }
+        AbilityMember(symbol, _specialization) => {
+            // make lookup constraint to lookup this symbol's type in the environment
+            constraints.lookup(*symbol, expected, region)
+            // TODO: consider trying to solve `_specialization` here.
+        }
         Closure(ClosureData {
             function_type: fn_var,
             closure_type: closure_var,
@@ -998,7 +1003,13 @@ pub fn constrain_expr(
 
             let opaque_type = Type::Alias {
                 symbol: *name,
-                type_arguments: type_arguments.iter().copied().map(Type::Variable).collect(),
+                type_arguments: type_arguments
+                    .iter()
+                    .map(|v| OptAbleType {
+                        typ: Type::Variable(v.var),
+                        opt_ability: v.opt_ability,
+                    })
+                    .collect(),
                 lambda_set_variables: lambda_set_variables.clone(),
                 actual: Box::new(arg_type.clone()),
                 kind: AliasKind::Opaque,
@@ -1035,7 +1046,7 @@ pub fn constrain_expr(
 
             let mut vars = vec![*arg_var, *opaque_var];
             // Also add the fresh variables we created for the type argument and lambda sets
-            vars.extend(type_arguments);
+            vars.extend(type_arguments.iter().map(|v| v.var));
             vars.extend(lambda_set_variables.iter().map(|v| {
                 v.0.expect_variable("all lambda sets should be fresh variables here")
             }));
@@ -1471,8 +1482,8 @@ fn constrain_typed_def(
 
             constrain_def_make_constraint(
                 constraints,
-                new_rigid_variables,
-                new_infer_variables,
+                new_rigid_variables.into_iter(),
+                new_infer_variables.into_iter(),
                 expr_con,
                 body_con,
                 def_pattern_state,
@@ -1506,8 +1517,8 @@ fn constrain_typed_def(
 
             constrain_def_make_constraint(
                 constraints,
-                new_rigid_variables,
-                new_infer_variables,
+                new_rigid_variables.into_iter(),
+                new_infer_variables.into_iter(),
                 expr_con,
                 body_con,
                 def_pattern_state,
@@ -1672,8 +1683,8 @@ fn constrain_def(
 
             constrain_def_make_constraint(
                 constraints,
-                vec![],
-                vec![],
+                std::iter::empty(),
+                std::iter::empty(),
                 expr_con,
                 body_con,
                 def_pattern_state,
@@ -1684,8 +1695,8 @@ fn constrain_def(
 
 pub fn constrain_def_make_constraint(
     constraints: &mut Constraints,
-    new_rigid_variables: Vec<Variable>,
-    new_infer_variables: Vec<Variable>,
+    new_rigid_variables: impl Iterator<Item = Variable>,
+    new_infer_variables: impl Iterator<Item = Variable>,
     expr_con: Constraint,
     body_con: Constraint,
     def_pattern_state: PatternState,
diff --git a/compiler/constrain/src/module.rs b/compiler/constrain/src/module.rs
index 0051a7049e..ec913f44cd 100644
--- a/compiler/constrain/src/module.rs
+++ b/compiler/constrain/src/module.rs
@@ -1,3 +1,4 @@
+use crate::expr::{constrain_def_make_constraint, constrain_def_pattern, Env};
 use roc_builtins::std::StdLib;
 use roc_can::abilities::AbilitiesStore;
 use roc_can::constraint::{Constraint, Constraints};
@@ -12,8 +13,6 @@ use roc_types::solved_types::{FreeVars, SolvedType};
 use roc_types::subs::{VarStore, Variable};
 use roc_types::types::{AnnotationSource, Category, Type};
 
-use crate::expr::{constrain_def_make_constraint, constrain_def_pattern, Env};
-
 /// The types of all exposed values/functions of a collection of modules
 #[derive(Clone, Debug, Default)]
 pub struct ExposedByModule {
@@ -105,7 +104,7 @@ pub fn constrain_module(
     let constraint = crate::expr::constrain_decls(constraints, home, declarations);
     let constraint =
         constrain_symbols_from_requires(constraints, symbols_from_requires, home, constraint);
-    let constraint = frontload_ability_constraints(constraints, abilities_store, constraint);
+    let constraint = frontload_ability_constraints(constraints, abilities_store, home, constraint);
 
     // The module constraint should always save the environment at the end.
     debug_assert!(constraints.contains_save_the_environment(&constraint));
@@ -140,8 +139,8 @@ fn constrain_symbols_from_requires(
                     constraints,
                     // No new rigids or flex vars because they are represented in the type
                     // annotation.
-                    vec![],
-                    vec![],
+                    std::iter::empty(),
+                    std::iter::empty(),
                     Constraint::True,
                     constraint,
                     def_pattern_state,
@@ -170,39 +169,44 @@ fn constrain_symbols_from_requires(
 pub fn frontload_ability_constraints(
     constraints: &mut Constraints,
     abilities_store: &AbilitiesStore,
+    home: ModuleId,
     mut constraint: Constraint,
 ) -> Constraint {
     for (member_name, member_data) in abilities_store.root_ability_members().iter() {
-        // 1. Attach the type of member signature to the reserved signature_var. This is
-        //    infallible.
-        let unify_with_signature_var = constraints.equal_types_var(
-            member_data.signature_var,
-            Expected::NoExpectation(member_data.signature.clone()),
-            Category::Storage(std::file!(), std::column!()),
-            Region::zero(),
+        let rigids = Default::default();
+        let env = Env { home, rigids };
+        let pattern = Loc::at_zero(roc_can::pattern::Pattern::Identifier(*member_name));
+
+        let mut def_pattern_state = constrain_def_pattern(
+            constraints,
+            &env,
+            &pattern,
+            Type::Variable(member_data.signature_var),
         );
 
-        // 2. Store the member signature on the member symbol. This makes sure we generalize it on
-        //    the toplevel, as appropriate.
-        let vars = &member_data.variables;
-        let rigids = (vars.rigid_vars.iter())
-            // For our purposes, in the let constraint, able vars are treated like rigids.
-            .chain(vars.able_vars.iter())
-            .copied();
-        let flex = vars.flex_vars.iter().copied();
+        def_pattern_state.vars.push(member_data.signature_var);
 
-        let let_constr = constraints.let_constraint(
-            rigids,
-            flex,
-            [(
-                *member_name,
-                Loc::at_zero(Type::Variable(member_data.signature_var)),
-            )],
+        let vars = &member_data.variables;
+        let rigid_variables = vars.rigid_vars.iter().chain(vars.able_vars.iter()).copied();
+        let infer_variables = vars.flex_vars.iter().copied();
+
+        def_pattern_state
+            .constraints
+            .push(constraints.equal_types_var(
+                member_data.signature_var,
+                Expected::NoExpectation(member_data.signature.clone()),
+                Category::Storage(file!(), line!()),
+                Region::zero(),
+            ));
+
+        constraint = constrain_def_make_constraint(
+            constraints,
+            rigid_variables,
+            infer_variables,
             Constraint::True,
             constraint,
+            def_pattern_state,
         );
-
-        constraint = constraints.and_constraint([unify_with_signature_var, let_constr]);
     }
     constraint
 }
diff --git a/compiler/constrain/src/pattern.rs b/compiler/constrain/src/pattern.rs
index b2dde1ae63..19d552ddf4 100644
--- a/compiler/constrain/src/pattern.rs
+++ b/compiler/constrain/src/pattern.rs
@@ -10,7 +10,8 @@ use roc_module::symbol::Symbol;
 use roc_region::all::{Loc, Region};
 use roc_types::subs::Variable;
 use roc_types::types::{
-    AliasKind, Category, PReason, PatternCategory, Reason, RecordField, Type, TypeExtension,
+    AliasKind, Category, OptAbleType, PReason, PatternCategory, Reason, RecordField, Type,
+    TypeExtension,
 };
 
 #[derive(Default)]
@@ -514,7 +515,13 @@ pub fn constrain_pattern(
 
             let opaque_type = Type::Alias {
                 symbol: *opaque,
-                type_arguments: type_arguments.iter().copied().map(Type::Variable).collect(),
+                type_arguments: type_arguments
+                    .iter()
+                    .map(|v| OptAbleType {
+                        typ: Type::Variable(v.var),
+                        opt_ability: v.opt_ability,
+                    })
+                    .collect(),
                 lambda_set_variables: lambda_set_variables.clone(),
                 actual: Box::new(arg_pattern_type.clone()),
                 kind: AliasKind::Opaque,
@@ -571,7 +578,7 @@ pub fn constrain_pattern(
                 .vars
                 .extend_from_slice(&[*arg_pattern_var, *whole_var]);
             // Also add the fresh variables we created for the type argument and lambda sets
-            state.vars.extend(type_arguments);
+            state.vars.extend(type_arguments.iter().map(|v| v.var));
             state.vars.extend(lambda_set_variables.iter().map(|v| {
                 v.0.expect_variable("all lambda sets should be fresh variables here")
             }));
diff --git a/compiler/load_internal/src/file.rs b/compiler/load_internal/src/file.rs
index 62b1189f77..454f7e2493 100644
--- a/compiler/load_internal/src/file.rs
+++ b/compiler/load_internal/src/file.rs
@@ -4107,7 +4107,7 @@ fn make_specializations<'a>(
     specializations_we_must_make: Vec<ExternalSpecializations>,
     mut module_timing: ModuleTiming,
     target_info: TargetInfo,
-    abilities_store: AbilitiesStore,
+    mut abilities_store: AbilitiesStore,
 ) -> Msg<'a> {
     let make_specializations_start = SystemTime::now();
     let mut mono_problems = Vec::new();
@@ -4123,7 +4123,7 @@ fn make_specializations<'a>(
         update_mode_ids: &mut update_mode_ids,
         // call_specialization_counter=0 is reserved
         call_specialization_counter: 1,
-        abilities_store: &abilities_store,
+        abilities_store: &mut abilities_store,
     };
 
     let mut procs = Procs::new_in(arena);
@@ -4194,7 +4194,7 @@ fn build_pending_specializations<'a>(
     target_info: TargetInfo,
     // TODO remove
     exposed_to_host: ExposedToHost,
-    abilities_store: AbilitiesStore,
+    mut abilities_store: AbilitiesStore,
 ) -> Msg<'a> {
     let find_specializations_start = SystemTime::now();
 
@@ -4221,7 +4221,7 @@ fn build_pending_specializations<'a>(
         update_mode_ids: &mut update_mode_ids,
         // call_specialization_counter=0 is reserved
         call_specialization_counter: 1,
-        abilities_store: &abilities_store,
+        abilities_store: &mut abilities_store,
     };
 
     // Add modules' decls to Procs
diff --git a/compiler/mono/src/copy.rs b/compiler/mono/src/copy.rs
index 0895d0ca7f..0621d34061 100644
--- a/compiler/mono/src/copy.rs
+++ b/compiler/mono/src/copy.rs
@@ -67,6 +67,7 @@ pub fn deep_copy_type_vars_into_expr<'a>(
                 loc_elems: loc_elems.iter().map(|le| le.map(go_help)).collect(),
             },
             Var(sym) => Var(*sym),
+            AbilityMember(sym, specialization) => AbilityMember(*sym, *specialization),
             When {
                 loc_cond,
                 cond_var,
diff --git a/compiler/mono/src/ir.rs b/compiler/mono/src/ir.rs
index 75e3cf04de..afeb17efc4 100644
--- a/compiler/mono/src/ir.rs
+++ b/compiler/mono/src/ir.rs
@@ -7,10 +7,10 @@ use crate::layout::{
 use bumpalo::collections::{CollectIn, Vec};
 use bumpalo::Bump;
 use roc_builtins::bitcode::{FloatWidth, IntWidth};
-use roc_can::abilities::AbilitiesStore;
+use roc_can::abilities::{AbilitiesStore, SpecializationId};
 use roc_can::expr::{AnnotatedMark, ClosureData, IntValue};
 use roc_collections::all::{default_hasher, BumpMap, BumpMapDefault, MutMap};
-use roc_collections::VecMap;
+use roc_collections::{MutSet, VecMap};
 use roc_debug_flags::{
     dbg_do, ROC_PRINT_IR_AFTER_REFCOUNT, ROC_PRINT_IR_AFTER_RESET_REUSE,
     ROC_PRINT_IR_AFTER_SPECIALIZATION,
@@ -22,6 +22,7 @@ use roc_module::low_level::LowLevel;
 use roc_module::symbol::{IdentIds, ModuleId, Symbol};
 use roc_problem::can::{RuntimeError, ShadowKind};
 use roc_region::all::{Loc, Region};
+use roc_solve::ability::resolve_ability_specialization;
 use roc_std::RocDec;
 use roc_target::TargetInfo;
 use roc_types::subs::{
@@ -1253,7 +1254,7 @@ pub struct Env<'a, 'i> {
     pub target_info: TargetInfo,
     pub update_mode_ids: &'i mut UpdateModeIds,
     pub call_specialization_counter: u32,
-    pub abilities_store: &'i AbilitiesStore,
+    pub abilities_store: &'i mut AbilitiesStore,
 }
 
 impl<'a, 'i> Env<'a, 'i> {
@@ -2479,6 +2480,106 @@ fn generate_runtime_error_function<'a>(
     }
 }
 
+fn resolve_abilities_in_specialized_body<'a>(
+    env: &mut Env<'a, '_>,
+    procs: &Procs<'a>,
+    specialized_body: &roc_can::expr::Expr,
+    body_var: Variable,
+) -> std::vec::Vec<SpecializationId> {
+    use roc_can::expr::Expr;
+    use roc_can::traverse::{walk_expr, PatternVisitor, Visitor};
+    use roc_unify::unify::unify;
+
+    struct Resolver<'a> {
+        subs: &'a mut Subs,
+        procs: &'a Procs<'a>,
+        abilities_store: &'a mut AbilitiesStore,
+        seen_defs: MutSet<Symbol>,
+        specialized: std::vec::Vec<SpecializationId>,
+    }
+    impl PatternVisitor for Resolver<'_> {}
+    impl Visitor for Resolver<'_> {
+        fn visit_expr(&mut self, expr: &Expr, _region: Region, var: Variable) {
+            match expr {
+                Expr::Closure(..) => {
+                    // Don't walk down closure bodies. They will have their types refined when they
+                    // are themselves specialized, so we'll handle ability resolution in them at
+                    // that time too.
+                }
+                Expr::LetRec(..) | Expr::LetNonRec(..) => {
+                    // Also don't walk down let-bindings. These may be generalized and we won't
+                    // know their specializations until we collect them while building up the def.
+                    // So, we'll resolve any nested abilities when we know their specialized type
+                    // during def construction.
+                }
+                Expr::AbilityMember(member_sym, specialization_id) => {
+                    if self
+                        .abilities_store
+                        .get_resolved(*specialization_id)
+                        .is_some()
+                    {
+                        // We already know the specialization from type solving; we are good to go.
+                        return;
+                    }
+
+                    let specialization = resolve_ability_specialization(
+                        self.subs,
+                        self.abilities_store,
+                        *member_sym,
+                        var,
+                    )
+                    .expect("Ability specialization is unknown - code generation cannot proceed!");
+
+                    // We must now refine the current type state to account for this specialization,
+                    // since `var` may only have partial specialization information - enough to
+                    // figure out what specialization we need, but not the types of all arguments
+                    // and return types. So, unify with the variable with the specialization's type.
+                    let specialization_def = self
+                        .procs
+                        .partial_procs
+                        .get_symbol(specialization)
+                        .expect("Specialization found, but it's not in procs");
+                    let specialization_var = specialization_def.annotation;
+
+                    let unified = unify(self.subs, var, specialization_var, Mode::EQ);
+                    unified.expect_success(
+                        "Specialization does not unify - this is a typechecker bug!",
+                    );
+
+                    // Now walk the specialization def to pick up any more needed types. Of course,
+                    // we only want to pass through it once to avoid unbounded recursion.
+                    if !self.seen_defs.contains(&specialization) {
+                        self.visit_expr(
+                            &specialization_def.body,
+                            Region::zero(),
+                            specialization_def.body_var,
+                        );
+                        self.seen_defs.insert(specialization);
+                    }
+
+                    self.abilities_store
+                        .insert_resolved(*specialization_id, specialization);
+
+                    debug_assert!(!self.specialized.contains(specialization_id));
+                    self.specialized.push(*specialization_id);
+                }
+                _ => walk_expr(self, expr, var),
+            }
+        }
+    }
+
+    let mut specializer = Resolver {
+        subs: env.subs,
+        procs,
+        abilities_store: env.abilities_store,
+        seen_defs: MutSet::default(),
+        specialized: vec![],
+    };
+    specializer.visit_expr(specialized_body, Region::zero(), body_var);
+
+    specializer.specialized
+}
+
 fn specialize_external<'a>(
     env: &mut Env<'a, '_>,
     procs: &mut Procs<'a>,
@@ -2614,8 +2715,17 @@ fn specialize_external<'a>(
     };
 
     let body = partial_proc.body.clone();
+    let resolved_ability_specializations =
+        resolve_abilities_in_specialized_body(env, procs, &body, partial_proc.body_var);
+
     let mut specialized_body = from_can(env, partial_proc.body_var, body, procs, layout_cache);
 
+    // reset the resolved ability specializations so as not to interfere with other specializations
+    // of this proc.
+    resolved_ability_specializations
+        .into_iter()
+        .for_each(|sid| env.abilities_store.remove_resolved(sid));
+
     match specialized {
         SpecializedLayout::FunctionPointerBody {
             ret_layout,
@@ -3564,6 +3674,22 @@ pub fn with_hole<'a>(
 
             specialize_naked_symbol(env, variable, procs, layout_cache, assigned, hole, symbol)
         }
+        AbilityMember(_member, specialization_id) => {
+            let specialization_symbol = env
+                .abilities_store
+                .get_resolved(specialization_id)
+                .expect("Specialization was never made!");
+
+            specialize_naked_symbol(
+                env,
+                variable,
+                procs,
+                layout_cache,
+                assigned,
+                hole,
+                specialization_symbol,
+            )
+        }
         Tag {
             variant_var,
             name: tag_name,
@@ -4406,14 +4532,10 @@ pub fn with_hole<'a>(
                 // a proc in this module, or an imported symbol
                 procs.partial_procs.contains_key(key)
                     || (env.is_imported_symbol(key) && !procs.is_imported_module_thunk(key))
-                    || env.abilities_store.is_ability_member_name(key)
             };
 
             match loc_expr.value {
                 roc_can::expr::Expr::Var(proc_name) if is_known(proc_name) => {
-                    // This might be an ability member - if so, use the appropriate specialization.
-                    let proc_name = get_specialization(env, fn_var, proc_name).unwrap_or(proc_name);
-
                     // a call by a known name
                     call_by_name(
                         env,
@@ -4426,6 +4548,22 @@ pub fn with_hole<'a>(
                         hole,
                     )
                 }
+                roc_can::expr::Expr::AbilityMember(_, specialization_id) => {
+                    let proc_name = env.abilities_store.get_resolved(specialization_id).expect(
+                        "Ability specialization is unknown - code generation cannot proceed!",
+                    );
+
+                    call_by_name(
+                        env,
+                        procs,
+                        fn_var,
+                        proc_name,
+                        loc_args,
+                        layout_cache,
+                        assigned,
+                        hole,
+                    )
+                }
                 _ => {
                     // Call by pointer - the closure was anonymous, e.g.
                     //
@@ -4543,8 +4681,8 @@ pub fn with_hole<'a>(
                         }
                         UnspecializedExpr(symbol) => {
                             match procs.ability_member_aliases.get(symbol).unwrap() {
-                                &AbilityMember(member) => {
-                                    let proc_name = get_specialization(env, fn_var, member).expect("Recorded as an ability member, but it doesn't have a specialization");
+                                &self::AbilityMember(member) => {
+                                    let proc_name = resolve_ability_specialization(env.subs, env.abilities_store, member, fn_var).expect("Recorded as an ability member, but it doesn't have a specialization");
 
                                     // a call by a known name
                                     return call_by_name(
@@ -4904,45 +5042,6 @@ pub fn with_hole<'a>(
     }
 }
 
-#[inline(always)]
-fn get_specialization<'a>(
-    env: &mut Env<'a, '_>,
-    symbol_var: Variable,
-    symbol: Symbol,
-) -> Option<Symbol> {
-    use roc_solve::ability::type_implementing_member;
-    use roc_solve::solve::instantiate_rigids;
-    use roc_unify::unify::unify;
-
-    match env.abilities_store.member_def(symbol) {
-        None => {
-            // This is not an ability member, it doesn't need specialization.
-            None
-        }
-        Some(member) => {
-            let snapshot = env.subs.snapshot();
-            instantiate_rigids(env.subs, member.signature_var);
-            let (_, must_implement_ability) = unify(
-                env.subs,
-                symbol_var,
-                member.signature_var,
-                roc_unify::unify::Mode::EQ,
-            )
-            .expect_success("This typechecked previously");
-            env.subs.rollback_to(snapshot);
-            let specializing_type =
-                type_implementing_member(&must_implement_ability, member.parent_ability);
-
-            let specialization = env
-                .abilities_store
-                .get_specialization(symbol, specializing_type)
-                .expect("No specialization is recorded - I thought there would only be a type error here.");
-
-            Some(specialization.symbol)
-        }
-    }
-}
-
 #[allow(clippy::too_many_arguments)]
 fn construct_closure_data<'a, I>(
     env: &mut Env<'a, '_>,
@@ -5707,7 +5806,8 @@ pub fn from_can<'a>(
 
                         return from_can(env, variable, cont.value, procs, layout_cache);
                     }
-                    roc_can::expr::Expr::Var(original) => {
+                    roc_can::expr::Expr::Var(original)
+                    | roc_can::expr::Expr::AbilityMember(original, _) => {
                         // a variable is aliased, e.g.
                         //
                         //  foo = bar
@@ -5844,6 +5944,13 @@ pub fn from_can<'a>(
                             let _res =
                                 roc_unify::unify::unify(env.subs, var, def.expr_var, Mode::EQ);
 
+                            resolve_abilities_in_specialized_body(
+                                env,
+                                procs,
+                                &def.loc_expr.value,
+                                def.expr_var,
+                            );
+
                             return with_hole(
                                 env,
                                 def.loc_expr.value,
@@ -5875,6 +5982,13 @@ pub fn from_can<'a>(
                                     Mode::EQ,
                                 );
 
+                                resolve_abilities_in_specialized_body(
+                                    env,
+                                    procs,
+                                    &def.loc_expr.value,
+                                    def.expr_var,
+                                );
+
                                 stmt = with_hole(
                                     env,
                                     specialized_expr,
@@ -5933,6 +6047,13 @@ pub fn from_can<'a>(
                 let outer_symbol = env.unique_symbol();
                 stmt = store_pattern(env, procs, layout_cache, &mono_pattern, outer_symbol, stmt);
 
+                resolve_abilities_in_specialized_body(
+                    env,
+                    procs,
+                    &def.loc_expr.value,
+                    def.expr_var,
+                );
+
                 // convert the def body, store in outer_symbol
                 with_hole(
                     env,
@@ -6931,34 +7052,38 @@ fn can_reuse_symbol<'a>(
     procs: &Procs<'a>,
     expr: &roc_can::expr::Expr,
 ) -> ReuseSymbol {
+    use roc_can::expr::Expr::*;
     use ReuseSymbol::*;
 
-    if let roc_can::expr::Expr::Var(symbol) = expr {
-        let symbol = *symbol;
+    let symbol = match expr {
+        AbilityMember(_, specialization_id) => env
+            .abilities_store
+            .get_resolved(*specialization_id)
+            .expect("Specialization must be known!"),
+        Var(symbol) => *symbol,
+        _ => return NotASymbol,
+    };
 
-        let arguments = [
-            Symbol::ARG_1,
-            Symbol::ARG_2,
-            Symbol::ARG_3,
-            Symbol::ARG_4,
-            Symbol::ARG_5,
-            Symbol::ARG_6,
-            Symbol::ARG_7,
-        ];
+    let arguments = [
+        Symbol::ARG_1,
+        Symbol::ARG_2,
+        Symbol::ARG_3,
+        Symbol::ARG_4,
+        Symbol::ARG_5,
+        Symbol::ARG_6,
+        Symbol::ARG_7,
+    ];
 
-        if arguments.contains(&symbol) {
-            Value(symbol)
-        } else if env.is_imported_symbol(symbol) {
-            Imported(symbol)
-        } else if procs.partial_procs.contains_key(symbol) {
-            LocalFunction(symbol)
-        } else if procs.ability_member_aliases.get(symbol).is_some() {
-            UnspecializedExpr(symbol)
-        } else {
-            Value(symbol)
-        }
+    if arguments.contains(&symbol) {
+        Value(symbol)
+    } else if env.is_imported_symbol(symbol) {
+        Imported(symbol)
+    } else if procs.partial_procs.contains_key(symbol) {
+        LocalFunction(symbol)
+    } else if procs.ability_member_aliases.get(symbol).is_some() {
+        UnspecializedExpr(symbol)
     } else {
-        NotASymbol
+        Value(symbol)
     }
 }
 
@@ -6991,20 +7116,23 @@ fn handle_variable_aliasing<'a, BuildRest>(
 where
     BuildRest: FnOnce(&mut Env<'a, '_>, &mut Procs<'a>, &mut LayoutCache<'a>) -> Stmt<'a>,
 {
-    if env.abilities_store.is_ability_member_name(right) {
-        procs
-            .ability_member_aliases
-            .insert(left, AbilityMember(right));
-        return build_rest(env, procs, layout_cache);
-    }
-
-    if let Some(&ability_member) = procs.ability_member_aliases.get(right) {
-        // If `right` links to a partial expression, make sure we link `left` to it as well, so
-        // that usages of it will be specialized when building the rest of the program.
-        procs.ability_member_aliases.insert(left, ability_member);
-        return build_rest(env, procs, layout_cache);
+    // 1. Handle references to ability members - we could be aliasing an ability member, or another
+    //    alias to an ability member.
+    {
+        if env.abilities_store.is_ability_member_name(right) {
+            procs
+                .ability_member_aliases
+                .insert(left, AbilityMember(right));
+            return build_rest(env, procs, layout_cache);
+        }
+        if let Some(&ability_member) = procs.ability_member_aliases.get(right) {
+            procs.ability_member_aliases.insert(left, ability_member);
+            return build_rest(env, procs, layout_cache);
+        }
     }
 
+    // 2. Handle references to a known proc - again, we may be either aliasing the proc, or another
+    //    alias to a proc.
     if procs.partial_procs.contains_key(right) {
         // This is an alias to a function defined in this module.
         // Attach the alias, then build the rest of the module, so that we reference and specialize
@@ -7041,6 +7169,8 @@ where
         // then we must construct its closure; since imported symbols have no closure, we use the empty struct
         let_empty_struct(left, env.arena.alloc(result))
     } else {
+        // Otherwise, we are referencing a non-proc value.
+
         // We need to lift all specializations of "left" to be specializations of "right".
         let mut scratchpad_update_specializations = std::vec::Vec::new();
 
diff --git a/compiler/solve/src/ability.rs b/compiler/solve/src/ability.rs
index a9796590cf..fc51b01d37 100644
--- a/compiler/solve/src/ability.rs
+++ b/compiler/solve/src/ability.rs
@@ -7,6 +7,7 @@ use roc_types::types::{Category, PatternCategory};
 use roc_unify::unify::MustImplementAbility;
 use roc_unify::unify::MustImplementConstraints;
 
+use crate::solve::instantiate_rigids;
 use crate::solve::{IncompleteAbilityImplementation, TypeError};
 
 #[derive(Debug, Clone)]
@@ -170,12 +171,12 @@ pub fn type_implementing_member(
     ability: Symbol,
 ) -> Symbol {
     debug_assert_eq!({
-            let ability_implementations_for_specialization =
-                specialization_must_implement_constraints
-                    .clone()
-                    .get_unique();
-
-            ability_implementations_for_specialization.len()
+            specialization_must_implement_constraints
+                .clone()
+                .get_unique()
+                .into_iter()
+                .filter(|mia| mia.ability == ability)
+                .count()
         },
         1,
         "Multiple variables bound to an ability - this is ambiguous and should have been caught in canonicalization: {:?}",
@@ -188,3 +189,32 @@ pub fn type_implementing_member(
         .unwrap()
         .typ
 }
+
+pub fn resolve_ability_specialization(
+    subs: &mut Subs,
+    abilities_store: &AbilitiesStore,
+    ability_member: Symbol,
+    specialization_var: Variable,
+) -> Option<Symbol> {
+    use roc_unify::unify::{unify, Mode};
+
+    let member_def = abilities_store
+        .member_def(ability_member)
+        .expect("Not an ability member symbol");
+
+    let snapshot = subs.snapshot();
+    instantiate_rigids(subs, member_def.signature_var);
+    let (_, must_implement_ability) =
+        unify(subs, specialization_var, member_def.signature_var, Mode::EQ).expect_success(
+            "If resolving a specialization, the specialization must be known to typecheck.",
+        );
+
+    subs.rollback_to(snapshot);
+
+    let specializing_type =
+        type_implementing_member(&must_implement_ability, member_def.parent_ability);
+
+    let specialization = abilities_store.get_specialization(ability_member, specializing_type)?;
+
+    Some(specialization.symbol)
+}
diff --git a/compiler/solve/src/solve.rs b/compiler/solve/src/solve.rs
index 7c361f4ac6..a2a75cd146 100644
--- a/compiler/solve/src/solve.rs
+++ b/compiler/solve/src/solve.rs
@@ -17,8 +17,8 @@ use roc_types::subs::{
 };
 use roc_types::types::Type::{self, *};
 use roc_types::types::{
-    gather_fields_unsorted_iter, AliasCommon, AliasKind, Category, ErrorType, PatternCategory,
-    Reason, TypeExtension,
+    gather_fields_unsorted_iter, AliasCommon, AliasKind, Category, ErrorType, OptAbleType,
+    OptAbleVar, PatternCategory, Reason, TypeExtension,
 };
 use roc_unify::unify::{unify, Mode, Unified::*};
 
@@ -115,7 +115,7 @@ struct DelayedAliasVariables {
 }
 
 impl DelayedAliasVariables {
-    fn recursion_variables(self, variables: &mut [Variable]) -> &mut [Variable] {
+    fn recursion_variables(self, variables: &mut [OptAbleVar]) -> &mut [OptAbleVar] {
         let start = self.start as usize
             + (self.type_variables_len + self.lambda_set_variables_len) as usize;
         let length = self.recursion_variables_len as usize;
@@ -123,14 +123,14 @@ impl DelayedAliasVariables {
         &mut variables[start..][..length]
     }
 
-    fn lambda_set_variables(self, variables: &mut [Variable]) -> &mut [Variable] {
+    fn lambda_set_variables(self, variables: &mut [OptAbleVar]) -> &mut [OptAbleVar] {
         let start = self.start as usize + self.type_variables_len as usize;
         let length = self.lambda_set_variables_len as usize;
 
         &mut variables[start..][..length]
     }
 
-    fn type_variables(self, variables: &mut [Variable]) -> &mut [Variable] {
+    fn type_variables(self, variables: &mut [OptAbleVar]) -> &mut [OptAbleVar] {
         let start = self.start as usize;
         let length = self.type_variables_len as usize;
 
@@ -141,7 +141,7 @@ impl DelayedAliasVariables {
 #[derive(Debug, Default)]
 pub struct Aliases {
     aliases: Vec<(Symbol, Type, DelayedAliasVariables, AliasKind)>,
-    variables: Vec<Variable>,
+    variables: Vec<OptAbleVar>,
 }
 
 impl Aliases {
@@ -150,18 +150,28 @@ impl Aliases {
             {
                 let start = self.variables.len() as _;
 
-                self.variables
-                    .extend(alias.type_variables.iter().map(|x| x.value.1));
+                self.variables.extend(
+                    alias
+                        .type_variables
+                        .iter()
+                        .map(|x| OptAbleVar::from(&x.value)),
+                );
 
                 self.variables.extend(alias.lambda_set_variables.iter().map(
                     |x| match x.as_inner() {
-                        Type::Variable(v) => *v,
+                        Type::Variable(v) => OptAbleVar::unbound(*v),
                         _ => unreachable!("lambda set type is not a variable"),
                     },
                 ));
 
                 let recursion_variables_len = alias.recursion_variables.len() as _;
-                self.variables.extend(alias.recursion_variables);
+                self.variables.extend(
+                    alias
+                        .recursion_variables
+                        .iter()
+                        .copied()
+                        .map(OptAbleVar::unbound),
+                );
 
                 DelayedAliasVariables {
                     start,
@@ -303,10 +313,14 @@ impl Aliases {
 
         let mut substitutions: MutMap<_, _> = Default::default();
 
-        for rec_var in delayed_variables
+        for OptAbleVar {
+            var: rec_var,
+            opt_ability,
+        } in delayed_variables
             .recursion_variables(&mut self.variables)
             .iter_mut()
         {
+            debug_assert!(opt_ability.is_none());
             let new_var = subs.fresh_unnamed_flex_var();
             substitutions.insert(*rec_var, new_var);
             *rec_var = new_var;
@@ -318,10 +332,10 @@ impl Aliases {
         for (old, new) in old_type_variables.iter_mut().zip(new_type_variables) {
             // if constraint gen duplicated a type these variables could be the same
             // (happens very often in practice)
-            if *old != *new {
-                substitutions.insert(*old, *new);
+            if old.var != *new {
+                substitutions.insert(old.var, *new);
 
-                *old = *new;
+                old.var = *new;
             }
         }
 
@@ -333,9 +347,10 @@ impl Aliases {
             .iter_mut()
             .zip(new_lambda_set_variables)
         {
-            if *old != *new {
-                substitutions.insert(*old, *new);
-                *old = *new;
+            debug_assert!(old.opt_ability.is_none());
+            if old.var != *new {
+                substitutions.insert(old.var, *new);
+                old.var = *new;
             }
         }
 
@@ -1937,8 +1952,39 @@ fn type_to_variable<'a>(
                     let length = type_arguments.len() + lambda_set_variables.len();
                     let new_variables = VariableSubsSlice::reserve_into_subs(subs, length);
 
-                    for (target_index, arg_type) in (new_variables.indices()).zip(type_arguments) {
-                        let copy_var = helper!(arg_type);
+                    for (target_index, OptAbleType { typ, opt_ability }) in
+                        (new_variables.indices()).zip(type_arguments)
+                    {
+                        let copy_var = match opt_ability {
+                            None => helper!(typ),
+                            Some(ability) => {
+                                // If this type argument is marked as being bound to an ability, we must
+                                // now correctly instantiate it as so.
+                                match RegisterVariable::from_type(subs, rank, pools, arena, typ) {
+                                    RegisterVariable::Direct(var) => {
+                                        use Content::*;
+                                        match *subs.get_content_without_compacting(var) {
+                                            FlexVar(opt_name) => subs
+                                                .set_content(var, FlexAbleVar(opt_name, *ability)),
+                                            RigidVar(..) => internal_error!("Rigid var in type arg for {:?} - this is a bug in the solver, or our understanding", actual),
+                                            RigidAbleVar(..) | FlexAbleVar(..) => internal_error!("Able var in type arg for {:?} - this is a bug in the solver, or our understanding", actual),
+                                            _ => {
+                                                // TODO associate the type to the bound ability, and check
+                                                // that it correctly implements the ability.
+                                            }
+                                        }
+                                        var
+                                    }
+                                    RegisterVariable::Deferred => {
+                                        // TODO associate the type to the bound ability, and check
+                                        // that it correctly implements the ability.
+                                        let var = subs.fresh_unnamed_flex_var();
+                                        stack.push(TypeToVar::Defer(typ, var));
+                                        var
+                                    }
+                                }
+                            }
+                        };
                         subs.variables[target_index] = copy_var;
                     }
 
diff --git a/compiler/solve/tests/solve_expr.rs b/compiler/solve/tests/solve_expr.rs
index a161271d74..3b37623caf 100644
--- a/compiler/solve/tests/solve_expr.rs
+++ b/compiler/solve/tests/solve_expr.rs
@@ -25,7 +25,8 @@ mod solve_expr {
     // HELPERS
 
     lazy_static! {
-        static ref RE_TYPE_QUERY: Regex = Regex::new(r#"^\s*#\s*(?P<where>\^+)\s*$"#).unwrap();
+        static ref RE_TYPE_QUERY: Regex =
+            Regex::new(r#"(?P<where>\^+)(?:\{-(?P<sub>\d+)\})?"#).unwrap();
     }
 
     #[derive(Debug, Clone, Copy)]
@@ -35,9 +36,14 @@ mod solve_expr {
         let line_info = LineInfo::new(src);
         let mut queries = vec![];
         for (i, line) in src.lines().enumerate() {
-            if let Some(capture) = RE_TYPE_QUERY.captures(line) {
+            for capture in RE_TYPE_QUERY.captures_iter(line) {
                 let wher = capture.name("where").unwrap();
+                let subtract_col = capture
+                    .name("sub")
+                    .and_then(|m| str::parse(m.as_str()).ok())
+                    .unwrap_or(0);
                 let (start, end) = (wher.start() as u32, wher.end() as u32);
+                let (start, end) = (start - subtract_col, end - subtract_col);
                 let last_line = i as u32 - 1;
                 let start_lc = LineColumn {
                     line: last_line,
@@ -273,7 +279,8 @@ mod solve_expr {
             let start = region.start().offset;
             let end = region.end().offset;
             let text = &src[start as usize..end as usize];
-            let var = find_type_at(region, &decls).expect(&format!("No type for {}!", &text));
+            let var = find_type_at(region, &decls)
+                .expect(&format!("No type for {} ({:?})!", &text, region));
 
             name_all_type_vars(var, subs);
             let content = subs.get_content_without_compacting(var);
@@ -6232,7 +6239,7 @@ mod solve_expr {
                 "#
             ),
             "F b -> b",
-        )
+        );
     }
 
     #[test]
@@ -6252,4 +6259,129 @@ mod solve_expr {
             "MyResult",
         )
     }
+
+    #[test]
+    fn alias_propagates_able_var() {
+        infer_eq_without_problem(
+            indoc!(
+                r#"
+                app "test" provides [ zeroEncoder ] to "./platform"
+
+                Encoder fmt := List U8, fmt -> List U8 | fmt has Format
+
+                Format has it : fmt -> {} | fmt has Format
+
+                zeroEncoder = @Encoder \lst, _ -> lst
+                "#
+            ),
+            "Encoder a | a has Format",
+        )
+    }
+
+    #[test]
+    fn encoder() {
+        infer_queries(
+            indoc!(
+                r#"
+                app "test" provides [ myU8Bytes ] to "./platform"
+
+                Encoder fmt := List U8, fmt -> List U8 | fmt has Format
+
+                Encoding has
+                  toEncoder : val -> Encoder fmt | val has Encoding, fmt has Format
+
+                Format has
+                  u8 : U8 -> Encoder fmt | fmt has Format
+
+                appendWith : List U8, Encoder fmt, fmt -> List U8 | fmt has Format
+                appendWith = \lst, (@Encoder doFormat), fmt -> doFormat lst fmt
+
+                toBytes : val, fmt -> List U8 | val has Encoding, fmt has Format
+                toBytes = \val, fmt -> appendWith [] (toEncoder val) fmt
+
+
+                Linear := {}
+
+                # impl Format for Linear
+                u8 = \n -> @Encoder (\lst, @Linear {} -> List.append lst n)
+                #^^{-1}
+
+                MyU8 := U8
+
+                # impl Encoding for MyU8
+                toEncoder = \@MyU8 n -> u8 n
+                #^^^^^^^^^{-1}
+
+                myU8Bytes = toBytes (@MyU8 15) (@Linear {})
+                #^^^^^^^^^{-1}
+                "#
+            ),
+            &[
+                "u8 : U8 -> Encoder Linear",
+                "toEncoder : MyU8 -> Encoder fmt | fmt has Format",
+                "myU8Bytes : List U8",
+            ],
+        )
+    }
+
+    #[test]
+    fn decoder() {
+        infer_queries(
+            indoc!(
+                r#"
+                app "test" provides [ myU8 ] to "./platform"
+
+                DecodeError : [ TooShort, Leftover (List U8) ]
+
+                Decoder val fmt := List U8, fmt -> { result: Result val DecodeError, rest: List U8 } | fmt has DecoderFormatting
+
+                Decoding has
+                    decoder : Decoder val fmt | val has Decoding, fmt has DecoderFormatting
+
+                DecoderFormatting has
+                    u8 : Decoder U8 fmt | fmt has DecoderFormatting
+
+                decodeWith : List U8, Decoder val fmt, fmt -> { result: Result val DecodeError, rest: List U8 } | fmt has DecoderFormatting
+                decodeWith = \lst, (@Decoder doDecode), fmt -> doDecode lst fmt
+
+                fromBytes : List U8, fmt -> Result val DecodeError
+                            | fmt has DecoderFormatting, val has Decoding
+                fromBytes = \lst, fmt ->
+                    when decodeWith lst decoder fmt is
+                        { result, rest } ->
+                            when result is
+                                Ok val -> if List.isEmpty rest then Ok val else Err (Leftover rest)
+                                Err e -> Err e
+
+
+                Linear := {}
+
+                # impl DecoderFormatting for Linear
+                u8 = @Decoder \lst, @Linear {} ->
+                #^^{-1}
+                        when List.first lst is
+                            Ok n -> { result: Ok n, rest: List.dropFirst lst }
+                            Err _ -> { result: Err TooShort, rest: [] }
+
+                MyU8 := U8
+
+                # impl Decoding for MyU8
+                decoder = @Decoder \lst, fmt ->
+                #^^^^^^^{-1}
+                    when decodeWith lst u8 fmt is
+                        { result, rest } ->
+                            { result: Result.map result (\n -> @MyU8 n), rest }
+
+                myU8 : Result MyU8 _
+                myU8 = fromBytes [ 15 ] (@Linear {})
+                #^^^^{-1}
+                "#
+            ),
+            &[
+                "u8 : Decoder U8 Linear",
+                "decoder : Decoder MyU8 fmt | fmt has DecoderFormatting",
+                "myU8 : Result MyU8 DecodeError",
+            ],
+        )
+    }
 }
diff --git a/compiler/test_gen/src/gen_abilities.rs b/compiler/test_gen/src/gen_abilities.rs
index 4da1464de1..bd2fa3e852 100644
--- a/compiler/test_gen/src/gen_abilities.rs
+++ b/compiler/test_gen/src/gen_abilities.rs
@@ -10,6 +10,9 @@ use crate::helpers::wasm::assert_evals_to;
 #[cfg(test)]
 use indoc::indoc;
 
+#[cfg(test)]
+use roc_std::RocList;
+
 #[test]
 #[cfg(any(feature = "gen-llvm", feature = "gen-wasm"))]
 fn hash_specialization() {
@@ -216,3 +219,107 @@ fn ability_used_as_type_still_compiles() {
         u64
     )
 }
+
+#[test]
+#[cfg(any(feature = "gen-llvm"))]
+fn encode() {
+    assert_evals_to!(
+        indoc!(
+            r#"
+            app "test" provides [ myU8Bytes ] to "./platform"
+
+            Encoder fmt := List U8, fmt -> List U8 | fmt has Format
+
+            Encoding has
+              toEncoder : val -> Encoder fmt | val has Encoding, fmt has Format
+
+            Format has
+              u8 : U8 -> Encoder fmt | fmt has Format
+
+            appendWith : List U8, Encoder fmt, fmt -> List U8 | fmt has Format
+            appendWith = \lst, (@Encoder doFormat), fmt -> doFormat lst fmt
+
+            toBytes : val, fmt -> List U8 | val has Encoding, fmt has Format
+            toBytes = \val, fmt -> appendWith [] (toEncoder val) fmt
+
+
+            Linear := {} 
+
+            # impl Format for Linear
+            u8 = \n -> @Encoder (\lst, @Linear {} -> List.append lst n)
+
+            Rgba := { r : U8, g : U8, b : U8, a : U8 }
+
+            # impl Encoding for Rgba
+            toEncoder = \@Rgba {r, g, b, a} ->
+                @Encoder \lst, fmt -> lst
+                    |> appendWith (u8 r) fmt
+                    |> appendWith (u8 g) fmt
+                    |> appendWith (u8 b) fmt
+                    |> appendWith (u8 a) fmt
+
+            myU8Bytes = toBytes (@Rgba { r: 106, g: 90, b: 205, a: 255 }) (@Linear {})
+            "#
+        ),
+        RocList::from_slice(&[106, 90, 205, 255]),
+        RocList<u8>
+    )
+}
+
+#[test]
+#[cfg(any(feature = "gen-llvm"))]
+fn decode() {
+    assert_evals_to!(
+        indoc!(
+            r#"
+            app "test" provides [ myU8 ] to "./platform"
+
+            DecodeError : [ TooShort, Leftover (List U8) ]
+
+            Decoder val fmt := List U8, fmt -> { result: Result val DecodeError, rest: List U8 } | fmt has DecoderFormatting
+
+            Decoding has
+                decoder : Decoder val fmt | val has Decoding, fmt has DecoderFormatting
+
+            DecoderFormatting has
+                u8 : Decoder U8 fmt | fmt has DecoderFormatting
+
+            decodeWith : List U8, Decoder val fmt, fmt -> { result: Result val DecodeError, rest: List U8 } | fmt has DecoderFormatting
+            decodeWith = \lst, (@Decoder doDecode), fmt -> doDecode lst fmt
+
+            fromBytes : List U8, fmt -> Result val DecodeError
+                        | fmt has DecoderFormatting, val has Decoding
+            fromBytes = \lst, fmt ->
+                when decodeWith lst decoder fmt is
+                    { result, rest } ->
+                        Result.after result \val ->
+                            if List.isEmpty rest
+                            then Ok val
+                            else Err (Leftover rest)
+
+
+            Linear := {}
+
+            # impl DecoderFormatting for Linear
+            u8 = @Decoder \lst, @Linear {} ->
+                    when List.first lst is
+                        Ok n -> { result: Ok n, rest: List.dropFirst lst }
+                        Err _ -> { result: Err TooShort, rest: [] }
+
+            MyU8 := U8
+
+            # impl Decoding for MyU8
+            decoder = @Decoder \lst, fmt ->
+                { result, rest } = decodeWith lst u8 fmt
+                { result: Result.map result (\n -> @MyU8 n), rest }
+
+            myU8 =
+                when fromBytes [ 15 ] (@Linear {}) is
+                    Ok (@MyU8 n) -> n
+                    _ -> 27u8
+            "#
+        ),
+        15,
+        u8
+    );
+}
diff --git a/compiler/test_mono/src/tests.rs b/compiler/test_mono/src/tests.rs
index 859776724f..abdcc5b7b3 100644
--- a/compiler/test_mono/src/tests.rs
+++ b/compiler/test_mono/src/tests.rs
@@ -1344,6 +1344,38 @@ fn opaque_assign_to_symbol() {
     )
 }
 
+#[mono_test]
+fn encode() {
+    indoc!(
+        r#"
+        app "test" provides [ myU8Bytes ] to "./platform"
+
+        Encoder fmt := List U8, fmt -> List U8 | fmt has Format
+
+        Encoding has
+          toEncoder : val -> Encoder fmt | val has Encoding, fmt has Format
+
+        Format has
+          u8 : U8 -> Encoder fmt | fmt has Format
+
+
+        Linear := {}
+
+        # impl Format for Linear
+        u8 = \n -> @Encoder (\lst, @Linear {} -> List.append lst n)
+
+        MyU8 := U8
+
+        # impl Encoding for MyU8
+        toEncoder = \@MyU8 n -> u8 n
+
+        myU8Bytes =
+            when toEncoder (@MyU8 15) is
+                @Encoder doEncode -> doEncode [] (@Linear {})
+        "#
+    )
+}
+
 // #[ignore]
 // #[mono_test]
 // fn static_str_closure() {
diff --git a/compiler/types/src/pretty_print.rs b/compiler/types/src/pretty_print.rs
index b266edddb8..276a8ab2a1 100644
--- a/compiler/types/src/pretty_print.rs
+++ b/compiler/types/src/pretty_print.rs
@@ -116,7 +116,7 @@ fn find_names_needed(
     }
 
     match &subs.get_content_without_compacting(variable).clone() {
-        RecursionVar { opt_name: None, .. } | FlexVar(None) | FlexAbleVar(None, _) => {
+        RecursionVar { opt_name: None, .. } | FlexVar(None) => {
             let root = subs.get_root_key_without_compacting(variable);
 
             // If this var is *not* its own root, then the
@@ -135,6 +135,15 @@ fn find_names_needed(
                 }
             }
         }
+        FlexAbleVar(None, _) => {
+            let root = subs.get_root_key_without_compacting(variable);
+            if !root_appearances.contains_key(&root) {
+                roots.push(root);
+            }
+            // Able vars are always printed at least twice (in the signature, and in the "has"
+            // clause set).
+            root_appearances.insert(root, Appearances::Multiple);
+        }
         RecursionVar {
             opt_name: Some(name_index),
             ..
@@ -271,6 +280,11 @@ fn set_root_name(root: Variable, name: Lowercase, subs: &mut Subs) {
             let content = FlexVar(Some(name_index));
             subs.set_content(root, content);
         }
+        &FlexAbleVar(None, ability) => {
+            let name_index = SubsIndex::push_new(&mut subs.field_names, name);
+            let content = FlexAbleVar(Some(name_index), ability);
+            subs.set_content(root, content);
+        }
         RecursionVar {
             opt_name: None,
             structure,
diff --git a/compiler/types/src/solved_types.rs b/compiler/types/src/solved_types.rs
index 1f4eeb4f1c..7a899f6c46 100644
--- a/compiler/types/src/solved_types.rs
+++ b/compiler/types/src/solved_types.rs
@@ -1,5 +1,5 @@
 use crate::subs::{VarId, VarStore, Variable};
-use crate::types::{AliasKind, Problem, RecordField, Type, TypeExtension};
+use crate::types::{AliasKind, OptAbleType, Problem, RecordField, Type, TypeExtension};
 use roc_collections::all::{ImMap, SendMap};
 use roc_module::ident::{Lowercase, TagName};
 use roc_module::symbol::Symbol;
@@ -213,7 +213,11 @@ pub fn to_type(
             let mut type_variables = Vec::with_capacity(solved_type_variables.len());
 
             for solved_arg in solved_type_variables {
-                type_variables.push(to_type(solved_arg, free_vars, var_store));
+                type_variables.push(OptAbleType {
+                    typ: to_type(solved_arg, free_vars, var_store),
+                    // TODO: is this always correct?
+                    opt_ability: None,
+                });
             }
 
             let mut lambda_set_variables = Vec::with_capacity(solved_lambda_sets.len());
diff --git a/compiler/types/src/types.rs b/compiler/types/src/types.rs
index 92cfdd9020..0ba04ba799 100644
--- a/compiler/types/src/types.rs
+++ b/compiler/types/src/types.rs
@@ -191,6 +191,36 @@ pub struct AliasCommon {
     pub lambda_set_variables: Vec<LambdaSet>,
 }
 
+#[derive(Clone, Copy, Debug)]
+pub struct OptAbleVar {
+    pub var: Variable,
+    pub opt_ability: Option<Symbol>,
+}
+
+impl OptAbleVar {
+    pub fn unbound(var: Variable) -> Self {
+        Self {
+            var,
+            opt_ability: None,
+        }
+    }
+}
+
+#[derive(PartialEq, Eq, Debug)]
+pub struct OptAbleType {
+    pub typ: Type,
+    pub opt_ability: Option<Symbol>,
+}
+
+impl OptAbleType {
+    pub fn unbound(typ: Type) -> Self {
+        Self {
+            typ,
+            opt_ability: None,
+        }
+    }
+}
+
 #[derive(PartialEq, Eq)]
 pub enum Type {
     EmptyRec,
@@ -208,7 +238,7 @@ pub enum Type {
     DelayedAlias(AliasCommon),
     Alias {
         symbol: Symbol,
-        type_arguments: Vec<Type>,
+        type_arguments: Vec<OptAbleType>,
         lambda_set_variables: Vec<LambdaSet>,
         actual: Box<Type>,
         kind: AliasKind,
@@ -300,6 +330,16 @@ impl Clone for Type {
     }
 }
 
+impl Clone for OptAbleType {
+    fn clone(&self) -> Self {
+        // This passes through `Type`, so defer to that to bump the clone counter.
+        Self {
+            typ: self.typ.clone(),
+            opt_ability: self.opt_ability,
+        }
+    }
+}
+
 #[derive(PartialEq, Eq, Clone)]
 pub enum TypeExtension {
     Open(Box<Type>),
@@ -410,7 +450,10 @@ impl fmt::Debug for Type {
                 write!(f, "(Alias {:?}", symbol)?;
 
                 for arg in type_arguments {
-                    write!(f, " {:?}", arg)?;
+                    write!(f, " {:?}", &arg.typ)?;
+                    if let Some(ab) = arg.opt_ability {
+                        write!(f, ":{:?}", ab)?;
+                    }
                 }
 
                 for (lambda_set, greek_letter) in
@@ -709,7 +752,7 @@ impl Type {
                     ..
                 } => {
                     for value in type_arguments.iter_mut() {
-                        stack.push(value);
+                        stack.push(&mut value.typ);
                     }
 
                     for lambda_set in lambda_set_variables.iter_mut() {
@@ -818,7 +861,7 @@ impl Type {
                     ..
                 } => {
                     for value in type_arguments.iter_mut() {
-                        stack.push(value);
+                        stack.push(&mut value.typ);
                     }
                     for lambda_set in lambda_set_variables.iter_mut() {
                         stack.push(lambda_set.as_inner_mut());
@@ -915,7 +958,7 @@ impl Type {
                 ..
             } => {
                 for ta in type_arguments {
-                    ta.substitute_alias(rep_symbol, rep_args, actual)?;
+                    ta.typ.substitute_alias(rep_symbol, rep_args, actual)?;
                 }
                 alias_actual.substitute_alias(rep_symbol, rep_args, actual)
             }
@@ -1140,15 +1183,35 @@ impl Type {
                 lambda_set_variables,
                 actual: actual_type,
                 ..
+            } => {
+                for arg in type_args {
+                    arg.instantiate_aliases(region, aliases, var_store, new_lambda_set_variables);
+                }
+
+                for arg in lambda_set_variables {
+                    arg.instantiate_aliases(region, aliases, var_store, new_lambda_set_variables);
+                }
+
+                actual_type.instantiate_aliases(
+                    region,
+                    aliases,
+                    var_store,
+                    new_lambda_set_variables,
+                );
             }
-            | Alias {
+            Alias {
                 type_arguments: type_args,
                 lambda_set_variables,
                 actual: actual_type,
                 ..
             } => {
                 for arg in type_args {
-                    arg.instantiate_aliases(region, aliases, var_store, new_lambda_set_variables);
+                    arg.typ.instantiate_aliases(
+                        region,
+                        aliases,
+                        var_store,
+                        new_lambda_set_variables,
+                    );
                 }
 
                 for arg in lambda_set_variables {
@@ -1210,7 +1273,12 @@ impl Type {
                         // TODO substitute further in args
                         for (
                             Loc {
-                                value: (_, placeholder),
+                                value:
+                                    AliasVar {
+                                        var: placeholder,
+                                        opt_bound_ability,
+                                        ..
+                                    },
                                 ..
                             },
                             filler,
@@ -1223,7 +1291,10 @@ impl Type {
                                 var_store,
                                 new_lambda_set_variables,
                             );
-                            named_args.push(filler.clone());
+                            named_args.push(OptAbleType {
+                                typ: filler.clone(),
+                                opt_ability: *opt_bound_ability,
+                            });
                             substitution.insert(*placeholder, filler);
                         }
 
@@ -1509,7 +1580,7 @@ fn variables_help(tipe: &Type, accum: &mut ImSet<Variable>) {
             ..
         } => {
             for arg in type_arguments {
-                variables_help(arg, accum);
+                variables_help(&arg.typ, accum);
             }
             variables_help(actual, accum);
         }
@@ -1645,7 +1716,7 @@ fn variables_help_detailed(tipe: &Type, accum: &mut VariableDetail) {
             ..
         } => {
             for arg in type_arguments {
-                variables_help_detailed(arg, accum);
+                variables_help_detailed(&arg.typ, accum);
             }
             variables_help_detailed(actual, accum);
         }
@@ -1862,10 +1933,37 @@ pub enum AliasKind {
     Opaque,
 }
 
+#[derive(Clone, Debug, PartialEq)]
+pub struct AliasVar {
+    pub name: Lowercase,
+    pub var: Variable,
+    /// `Some` if this variable is bound to an ability; `None` otherwise.
+    pub opt_bound_ability: Option<Symbol>,
+}
+
+impl AliasVar {
+    pub fn unbound(name: Lowercase, var: Variable) -> AliasVar {
+        Self {
+            name,
+            var,
+            opt_bound_ability: None,
+        }
+    }
+}
+
+impl From<&AliasVar> for OptAbleVar {
+    fn from(av: &AliasVar) -> OptAbleVar {
+        OptAbleVar {
+            var: av.var,
+            opt_ability: av.opt_bound_ability,
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq)]
 pub struct Alias {
     pub region: Region,
-    pub type_variables: Vec<Loc<(Lowercase, Variable)>>,
+    pub type_variables: Vec<Loc<AliasVar>>,
 
     /// lambda set variables, e.g. the one annotating the arrow in
     /// a |c|-> b
diff --git a/compiler/unify/src/unify.rs b/compiler/unify/src/unify.rs
index 9a5ca9a28a..db4cf0b648 100644
--- a/compiler/unify/src/unify.rs
+++ b/compiler/unify/src/unify.rs
@@ -1813,11 +1813,12 @@ fn unify_flex(
     other: &Content,
 ) -> Outcome {
     match other {
-        FlexVar(None) => {
-            // If both are flex, and only left has a name, keep the name around.
+        FlexVar(other_opt_name) => {
+            // Prefer using right's name.
+            let opt_name = opt_name.or(*other_opt_name);
             match opt_able_bound {
-                Some(ability) => merge(subs, ctx, FlexAbleVar(*opt_name, ability)),
-                None => merge(subs, ctx, FlexVar(*opt_name)),
+                Some(ability) => merge(subs, ctx, FlexAbleVar(opt_name, ability)),
+                None => merge(subs, ctx, FlexVar(opt_name)),
             }
         }
 
@@ -1849,8 +1850,7 @@ fn unify_flex(
             }
         }
 
-        FlexVar(Some(_))
-        | RigidVar(_)
+        RigidVar(_)
         | RigidAbleVar(_, _)
         | RecursionVar { .. }
         | Structure(_)
@@ -1858,7 +1858,6 @@ fn unify_flex(
         | RangedNumber(..) => {
             // TODO special-case boolean here
             // In all other cases, if left is flex, defer to right.
-            // (This includes using right's name if both are flex and named.)
             merge(subs, ctx, *other)
         }
 
diff --git a/reporting/tests/helpers/mod.rs b/reporting/tests/helpers/mod.rs
index 9729112a75..4a429c4c5b 100644
--- a/reporting/tests/helpers/mod.rs
+++ b/reporting/tests/helpers/mod.rs
@@ -17,7 +17,7 @@ use roc_problem::can::Problem;
 use roc_region::all::Loc;
 use roc_solve::solve::{self, Aliases};
 use roc_types::subs::{Content, Subs, VarStore, Variable};
-use roc_types::types::Type;
+use roc_types::types::{AliasVar, Type};
 use std::hash::Hash;
 use std::path::{Path, PathBuf};
 
@@ -228,7 +228,10 @@ fn add_aliases(scope: &mut Scope, var_store: &mut VarStore) {
         let mut type_variables: Vec<_> = free_vars.unnamed_vars.into_iter().collect();
         type_variables.sort();
         for (loc_name, (_, var)) in vars.iter().zip(type_variables) {
-            variables.push(Loc::at(loc_name.region, (loc_name.value.clone(), var)));
+            variables.push(Loc::at(
+                loc_name.region,
+                AliasVar::unbound(loc_name.value.clone(), var),
+            ));
         }
 
         scope.add_alias(symbol, region, variables, typ, kind);
diff --git a/reporting/tests/test_reporting.rs b/reporting/tests/test_reporting.rs
index fa950fdaac..2fe63c75cc 100644
--- a/reporting/tests/test_reporting.rs
+++ b/reporting/tests/test_reporting.rs
@@ -9019,41 +9019,6 @@ I need all branches in an `if` to have the same type!
         )
     }
 
-    #[test]
-    fn alias_using_ability() {
-        new_report_problem_as(
-            "alias_using_ability",
-            indoc!(
-                r#"
-                app "test" provides [ a ] to "./platform"
-
-                Ability has ab : a -> {} | a has Ability
-
-                Alias : Ability
-
-                a : Alias
-                "#
-            ),
-            indoc!(
-                r#"
-                ── ALIAS USES ABILITY ──────────────────────────────────── /code/proj/Main.roc ─
-
-                The definition of the `Alias` aliases references the ability `Ability`:
-
-                5│  Alias : Ability
-                    ^^^^^
-
-                Abilities are not types, but you can add an ability constraint to a
-                type variable `a` by writing
-
-                    | a has Ability
-
-                 at the end of the type.
-                "#
-            ),
-        )
-    }
-
     #[test]
     fn ability_shadows_ability() {
         new_report_problem_as(
@@ -9130,37 +9095,6 @@ I need all branches in an `if` to have the same type!
         )
     }
 
-    #[test]
-    fn ability_member_binds_extra_ability() {
-        new_report_problem_as(
-            "ability_member_binds_extra_ability",
-            indoc!(
-                r#"
-                app "test" provides [ eq ] to "./platform"
-
-                Eq has eq : a, a -> Bool.Bool | a has Eq
-                Hash has hash : a, b -> Num.U64 | a has Eq, b has Hash
-                "#
-            ),
-            indoc!(
-                r#"
-                ── ABILITY MEMBER HAS EXTRANEOUS HAS CLAUSE ────────────── /code/proj/Main.roc ─
-
-                The definition of the ability member `hash` includes a has clause
-                binding an ability it is not a part of:
-
-                4│  Hash has hash : a, b -> Num.U64 | a has Eq, b has Hash
-                                                      ^^^^^^^^
-
-                Currently, ability members can only bind variables to the ability they
-                are a part of.
-
-                Hint: Did you mean to bind the `Hash` ability instead?
-                "#
-            ),
-        )
-    }
-
     #[test]
     fn ability_member_binds_parent_twice() {
         new_report_problem_as(