Merge pull request #2388 from unisonweb/fix/higher-rank

Pattern matching on constructors with polymorphic fields now works properly

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -1156,7 +1156,8 @@ checkCases scrutType outType cases@(Term.MatchCase _ _ t : _)
             vt = existentialp lo v
         appendContext [existential v]
         subtype (Type.effectV lo (lo, Type.effects lo es) (lo, vt)) sty
-      coalesceWanteds =<< traverse (checkCase scrutType outType) cases
+      scrutType' <- ungeneralize scrutType
+      coalesceWanteds =<< traverse (checkCase scrutType' outType) cases
 
 getEffect
   :: Var v => Ord loc => Reference -> Int -> M v loc (Type v loc)
@@ -1220,8 +1221,8 @@ checkPattern
   -> Pattern loc
   -> StateT [v] (M v loc) [(v, v)]
 checkPattern tx ty | (debugEnabled || debugPatternsEnabled) && traceShow ("checkPattern"::String, tx, ty) False = undefined
-checkPattern scrutineeType0 p =
-  lift (ungeneralize scrutineeType0) >>= \scrutineeType -> case p of
+checkPattern scrutineeType p =
+  case p of
     Pattern.Unbound _    -> pure []
     Pattern.Var     _loc -> do
       v  <- getAdvance p

unison-src/transcripts/higher-rank.md

@@ -0,0 +1,69 @@
+
+This transcript does some testing of higher-rank types. Regression tests related to higher-rank types can be added here.
+
+```ucm:hide
+.> alias.type ##Nat Nat
+.> alias.type ##Text Text
+.> alias.type ##IO IO
+```
+
+In this example, a higher-rank function is defined, `f`. No annotation is needed at the call-site of `f`, because the lambda is being checked against the polymorphic type `forall a . a -> a`, rather than inferred:
+
+```unison
+f : (forall a . a -> a) -> (Nat, Text)
+f id = (id 1, id "hi")
+
+> f (x -> x)
+```
+
+Another example, involving abilities. Here the ability-polymorphic function is instantiated with two different ability lists, `{}` and `{IO}`:
+
+```unison
+f : (forall a g . '{g} a -> '{g} a) -> () -> () 
+f id _ = 
+  (id ('1 : '{} Nat), id ('("hi") : '{IO} Text))
+  ()
+```
+
+Here's an example, showing that polymorphic functions can be fields of a constructor, and the functions remain polymorphic even when the field is bound to a name during pattern matching:
+
+```unison
+unique type Functor f = Functor (forall a b . (a -> b) -> f a -> f b)
+
+Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b)
+Functor.map = cases Functor f -> f
+
+Functor.blah : Functor f -> ()
+Functor.blah = cases Functor f -> 
+  g : forall a b . (a -> b) -> f a -> f b
+  g = f
+  ()
+```
+
+This example is similar, but involves abilities: 
+
+```unison
+unique ability Remote t where doRemoteStuff : ()
+unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a) 
+
+Loc.blah : Loc -> ()
+Loc.blah = cases Loc f ->
+  f0 : '{Remote tx} ax ->{Remote tx} tx ax
+  f0 = f
+  ()
+
+-- In this case, no annotation is needed since the lambda 
+-- is checked against a polymorphic type
+Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a) 
+             -> Loc -> Loc
+Loc.transform nt = cases Loc f -> Loc (a -> f (nt a))
+
+-- In this case, the annotation is needed since f' is inferred
+-- on its own it won't infer the higher-rank type
+Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a) 
+             -> Loc -> Loc
+Loc.transform2 nt = cases Loc f -> 
+  f' : forall t a . '{Remote t} a ->{Remote t} t a
+  f' a = f (nt a)
+  Loc f' 
+```

unison-src/transcripts/higher-rank.output.md

@@ -0,0 +1,126 @@
+
+This transcript does some testing of higher-rank types. Regression tests related to higher-rank types can be added here.
+
+In this example, a higher-rank function is defined, `f`. No annotation is needed at the call-site of `f`, because the lambda is being checked against the polymorphic type `forall a . a -> a`, rather than inferred:
+
+```unison
+f : (forall a . a -> a) -> (Nat, Text)
+f id = (id 1, id "hi")
+
+> f (x -> x)
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      f : (∀ a. a ->{g} a) ->{g} (Nat, Text)
+  
+  Now evaluating any watch expressions (lines starting with
+  `>`)... Ctrl+C cancels.
+
+    4 | > f (x -> x)
+          ⧩
+          (1, "hi")
+
+```
+Another example, involving abilities. Here the ability-polymorphic function is instantiated with two different ability lists, `{}` and `{IO}`:
+
+```unison
+f : (forall a g . '{g} a -> '{g} a) -> () -> () 
+f id _ = 
+  (id ('1 : '{} Nat), id ('("hi") : '{IO} Text))
+  ()
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      f : (∀ a g. '{g} a ->{h} '{g} a) -> '{h} ()
+
+```
+Here's an example, showing that polymorphic functions can be fields of a constructor, and the functions remain polymorphic even when the field is bound to a name during pattern matching:
+
+```unison
+unique type Functor f = Functor (forall a b . (a -> b) -> f a -> f b)
+
+Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b)
+Functor.map = cases Functor f -> f
+
+Functor.blah : Functor f -> ()
+Functor.blah = cases Functor f -> 
+  g : forall a b . (a -> b) -> f a -> f b
+  g = f
+  ()
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      unique type Functor f
+      Functor.blah : Functor f -> ()
+      Functor.map  : Functor f
+                     -> (∀ a b. (a -> b) -> f a -> f b)
+
+```
+This example is similar, but involves abilities: 
+
+```unison
+unique ability Remote t where doRemoteStuff : ()
+unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a) 
+
+Loc.blah : Loc -> ()
+Loc.blah = cases Loc f ->
+  f0 : '{Remote tx} ax ->{Remote tx} tx ax
+  f0 = f
+  ()
+
+-- In this case, no annotation is needed since the lambda 
+-- is checked against a polymorphic type
+Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a) 
+             -> Loc -> Loc
+Loc.transform nt = cases Loc f -> Loc (a -> f (nt a))
+
+-- In this case, the annotation is needed since f' is inferred
+-- on its own it won't infer the higher-rank type
+Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a) 
+             -> Loc -> Loc
+Loc.transform2 nt = cases Loc f -> 
+  f' : forall t a . '{Remote t} a ->{Remote t} t a
+  f' a = f (nt a)
+  Loc f' 
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      unique type Loc
+      unique ability Remote t
+      Loc.blah       : Loc -> ()
+      Loc.transform  : (∀ t a. '{Remote t} a -> '{Remote t} a)
+                       -> Loc
+                       -> Loc
+      Loc.transform2 : (∀ t a. '{Remote t} a -> '{Remote t} a)
+                       -> Loc
+                       -> Loc
+
+```