fix: Don't refine already refined skolems

base/src/scoped_map.rs

@@ -160,15 +160,9 @@ impl<K: Eq + Hash + Clone, V> ScopedMap<K, V> {
         self.get(k).is_some()
     }
 
-    /// Returns the number of elements in the container.
-    /// Shadowed elements are not counted
-    pub fn len(&self) -> usize {
-        self.map.len()
-    }
-
     /// Returns the number of elements in the container.
     /// Shadowed elements are counted
-    pub fn full_len(&self) -> usize {
+    pub fn len(&self) -> usize {
         self.map.values().map(|v| v.len()).sum()
     }
 

check/src/typecheck.rs

@@ -2733,7 +2733,7 @@ impl<'a, 'ast> Typecheck<'a, 'ast> {
     ) -> RcType {
         debug!("Refine {} : {}", expected, actual);
         types::walk_type(&actual, &mut |typ: &RcType| {
-            if let Type::Skolem(skolem) = &**typ {
+            if let Type::Skolem(skolem) = &**self.subs.real(typ) {
                 self.refined_variables.entry(skolem.id).or_insert(());
             }
         });

check/tests/pass.rs

@@ -1135,3 +1135,40 @@ match writer with
     "#,
     "test.List String"
 }
+
+test_check! {
+    issue_842,
+    r#"
+type Digit a =
+    | One a
+    | Two a a
+
+type Node b =
+    | Node2 b b
+
+type FingerTree c =
+    | Empty
+    | Single c
+    | Deep (Digit c) (FingerTree (Node c)) (Digit c)
+
+type View d =
+    | Nil
+    | View d (FingerTree d)
+
+rec
+let viewl xs : FingerTree e -> View e =
+    match xs with
+    | Empty -> Nil
+    | Single x -> View x Empty
+    | Deep (One a) deeper suffix ->
+        match viewl deeper with
+        | View (Node2 b c) rest -> View a (Deep (Two b c) rest suffix)
+        | Nil ->
+            match suffix with
+            | One w -> View a (Single w)
+in
+
+viewl
+    "#,
+    "forall a . test.FingerTree a -> test.View a"
+}