From 30df63f5051e44fd44fefbcda5d99d7477913e76 Mon Sep 17 00:00:00 2001
From: Markus Westerlind <marwes91@gmail.com>
Date: Fri, 25 Dec 2020 21:47:21 +0100
Subject: [PATCH 1/2] Correct ScopedMap::len

---
 base/src/scoped_map.rs | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/base/src/scoped_map.rs b/base/src/scoped_map.rs
index 28288272d0..622d575838 100644
--- a/base/src/scoped_map.rs
+++ b/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()
     }
 

From f39b39658d9b01c7e503a1a519ce5f134127b1bd Mon Sep 17 00:00:00 2001
From: Markus Westerlind <marwes91@gmail.com>
Date: Fri, 25 Dec 2020 21:47:56 +0100
Subject: [PATCH 2/2] fix: Don't refine already refined skolems

Fixes #842
---
 check/src/typecheck.rs |  2 +-
 check/tests/pass.rs    | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/check/src/typecheck.rs b/check/src/typecheck.rs
index d1bccd31d7..de7a0798b8 100644
--- a/check/src/typecheck.rs
+++ b/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(());
             }
         });
diff --git a/check/tests/pass.rs b/check/tests/pass.rs
index f230cc4f5f..9ff26c6108 100644
--- a/check/tests/pass.rs
+++ b/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"
+}