Mention 'amc explain' in error messages

* And: warn about #219

doc/errors.txt

@@ -51,6 +51,7 @@ types/2036.txt TC: MightNotTerminate
 types/2037.txt TC: TyFunInLhs
 types/2038.txt TC: DICan'tDerive
 types/2039.txt TC: NotAnIdiom
+types/2040.txt TC: PolyTyFunRhs
 verify/3001.txt Verify: MalformedRecursiveRhs
 verify/3002.txt Verify: DefinedUnused
 verify/3003.txt Verify: ParseErrorInForeign

doc/errors/types/2040.txt

@@ -0,0 +1,84 @@
+Type functions with polymorphic (`forall .` or `forall ->`) headed types
+do not play nicely with how the Amulet type checker is implemented
+internally. Thus, using these types in practice might be a bit
+complicated.
+
+    type function foo ('x : bool) begin
+      foo true  = forall 'a. 'a -> 'a
+      foo false = ()
+    end
+
+    type sbool 'x =
+      | STrue  : sbool true
+      | SFalse : sbool false
+
+    let
+      foo :
+        forall 'b. sbool 'b -> foo 'b -> ()
+      =
+        fun x y ->
+          match x with
+          | STrue -> y ()
+          | SFalse -> y
+
+This program certainly looks reasonable, and one might reasonably expect
+it to type-check. But consider what happens when type-checking the
+branch
+
+    | STrue -> y ()
+
+The way type checking Amulet proceeds is by building up a set of
+constraints by walking over the term, then solving them afterwards, to
+support the more complex type system features (like GADTs and type
+functions, both of which are at play here).
+
+When amc sees an application like `y ()`, what it does is (roughly) as
+following:
+
+1. Assign an unknown type `alpha` for y
+2. Since `y` is used in an application, `alpha` must really be equal to
+`beta -> gamma` (for some unknown `beta`, `gamma`)
+3. The argument to `y` is `()`, so `beta` must be equal to `()`
+
+Solving these constraints, we arrive at the type `() -> gamma` for the
+term `y`.
+
+Back to the branch `| STrue -> y ()`, amc will see that `y` is used in a
+function position and infer a type like `alpha -> beta` for it, which is
+wrong. When generating constraints for the branch, amc doesn't yet know
+that `y` has type `forall 'a. 'a -> 'a`; It knows is `y : foo b`
+(from the type signature) and that `b ~ true` (from matching on STrue),
+but it hasn't quite pieced this information together to arrive at
+`y : forall 'a. 'a -> 'a`: that's what the solver does!
+
+A possible fix is to "invert" the pattern matching as follows:
+
+    let
+      foo :
+        forall 'b. sbool 'b -> foo 'b -> ()
+      =
+        function
+          | STrue -> fun (y : forall 'a. 'a -> 'a) -> y ()
+          | SFalse -> fun y -> y
+
+Here, the GADT pattern matching scopes over the function expression
+`fun (y : forall 'a. 'a -> 'a)`, and we can indeed conclude from
+`b ~ true` that `foo b ~ forall 'a. 'a -> 'a`. Thus, `y` enters scope
+with a known polymorphic type, and inference can proceed.
+
+The reason that ascribing a type to `y` in the left-hand side doesn't
+work is that type ascriptions against polymorphic types will make all
+the bound type variables rigid and then check the term against a type
+with no quantifiers. For example:
+
+    (fun x -> x) : forall 'a. 'a -> 'a
+
+What happens is that first we _skolemise_ the type
+`forall 'a. 'a -> 'a`,
+returning a type with a rigid variable instead of `'a` (say `'A`). Then,
+we check the function expression against the type `'A -> 'A`.
+
+You can already see why `(y : forall 'a. 'a -> 'a)` won't work: We
+skolemise the type to `'A -> 'A` and then try unifying
+`forall 'a. 'a -> 'a` (from the expansion of `foo b` with `b ~ true`)
+with `'A -> 'A`, which fails.

doc/make_error_index.sh

@@ -30,7 +30,7 @@ cat errors.txt | while read -r file_desc; do
   printf "### E%.4d: \"%s\" {#%s}\n" $num $anchor $anchor >> $out
 
   cat errors/$fname | \
-    sed -re 's/`([ ,.])/`{.amulet}\1/g' \
+    sed -re 's/`([ ,.\):;])/`{.amulet}\1/g' \
     >> $out
 
   echo >> $out

src/Control/Monad/Infer.hs

@@ -161,6 +161,8 @@ data TypeError where
   TyFunInLhs :: SomeReason -> Type Typed -> TypeError
   NotAnIdiom :: Pretty (Var p) => Expr p -> TypeError
 
+  PolyTyFunRhs :: SomeReason -> Type Typed -> TypeError
+
 
 data WhatOverlaps = Overinst | Overeq Bool
 
@@ -580,6 +582,13 @@ instance Pretty TypeError where
   pretty (NotAnIdiom _) =
     vsep [ "This expression can not be used in an idiom bracket because it is not a function application" ]
 
+  pretty (PolyTyFunRhs _ tau) =
+    vsep [ "The right-hand-side of this type function equation is a polymorphic type."
+         , "This is technically unsupported, and might lead to strange type checking failures."
+         , "Offending type:"
+         , indent 2 (displayTypeTyped tau)
+         ]
+
   pretty (WarningError x) = pretty x
 
   pretty (UnsatClassCon _ (ConImplicit _ _ _ t) _) = string "No instance for" <+> pretty t
@@ -615,6 +624,7 @@ instance Spanned TypeError where
   annotation (OrphanInstance x _) = annotation x
   annotation (DIMalformedHead x) = annotation x
   annotation (DICan'tDerive _ x) = annotation x
+  annotation (PolyTyFunRhs x _) = annotation x
   annotation x = error (show (pretty x))
 
 instance Note TypeError Style where
@@ -624,6 +634,7 @@ instance Note TypeError Style where
   diagnosticKind DeadBranch{} = WarningMessage
   diagnosticKind MightNotTerminate{} = WarningMessage
   diagnosticKind AmbiguousType{} = WarningMessage
+  diagnosticKind PolyTyFunRhs{} = WarningMessage
   diagnosticKind WarningError{} = ErrorMessage
   diagnosticKind _ = ErrorMessage
 
@@ -934,6 +945,7 @@ instance Note TypeError Style where
   noteId DIMalformedHead{}    = Just 0008 -- This is a parse error that TC emits
   noteId DICan'tDerive{}      = Just 2038
   noteId NotAnIdiom{}         = Just 2039
+  noteId PolyTyFunRhs{}       = Just 2040
 
   noteId (Note x _) = noteId x
   noteId (Suggestion x _) = noteId x

src/Text/Pretty/Note.hs

@@ -72,12 +72,19 @@ format f x =
             NoteMessage -> annotate (NoteKind NoteMessage) "note"
             WarningMessage -> annotate (NoteKind WarningMessage) "warning"
             ErrorMessage -> annotate (NoteKind ErrorMessage) "error"
-      num = 
+      num =
         case noteId x of
           Just num -> parens (string (printf "%c%.4d" (toUpper (head (show c))) num))
           Nothing -> mempty
+      info =
+        case noteId x of
+          Just num -> (Right <$> formatSpan a <> colon)
+                  <+> string "Use amc explain"
+                  <+> (string (printf "%.4d" num))
+                  <+> string "for more information"
+          Nothing -> empty
       body = formatNote f x
-   in (Right <$> formatSpan a <> colon) <+> (Left <$> (c <+> num)) <##> body
+   in (Right <$> formatSpan a <> colon) <+> (Left <$> (c <+> num)) <##> body <##> info
 
 -- | Convert a note style to an ANSI style
 toAnsi :: NoteStyle -> AnsiStyle

src/Types/Infer/Function.hs

@@ -33,6 +33,8 @@ checkValidTypeFunction _ _ _ _ equations =
       familyFree (BecauseOf clause) lhs
       checkWildcard clause lhs
       checkWildcard clause rhs
+      when (isSkolemisable rhs) $
+        dictates (PolyTyFunRhs (BecauseOf clause) rhs)
     overlap mempty equations
     terminates equations
     pure ()

tests/amc/path.t

@@ -8,6 +8,7 @@ amc compile will extend the compile path
     │ 
   1 │ open import "my_lib.ml"
     │      ^^^^^^^^^^^^^^^^^^
+  tests/amc/files/import.ml[1:6 ..1:23]: Use amc explain 1010 for more information
 
   $ amc compile --lib tests/amc/lib tests/amc/files/import.ml
   do

tests/amc/prelude.t

@@ -16,6 +16,7 @@ Not using the prelude will fail
     │ 
   1 │ print "Hello"
     │ ^^^^^
+  =stdin[1:1 ..1:5]: Use amc explain 1001 for more information
   > 
 
 One can use a custom prelude

tests/lexer/context/unaligned_let.out

@@ -14,11 +14,13 @@ $end $end <eof>
     │             ^
   4 │           in x
     │           ^^
+  unaligned_let.ml[4:11 ..4:12]: Use amc explain 0012 for more information
   unaligned_let.ml[7:13 ..7:14]: warning (W0012)
     This `in` is misaligned with the corresponding `let`
     │ 
   6 │ let over = let x = 2
     │            ^
   7 │             in x
     │             ^^
+  unaligned_let.ml[7:13 ..7:14]: Use amc explain 0012 for more information
 *)

tests/lexer/fail_escape.out

@@ -3,15 +3,18 @@ fail_escape.ml[1:2 ..1:3]: error (E0011)
   │ 
 1 │ "\#  \0 \
   │  ^^
+fail_escape.ml[1:2 ..1:3]: Use amc explain 0011 for more information
 fail_escape.ml[1:6 ..1:7]: error (E0011)
   Unknown escape code.
   │ 
 1 │ "\#  \0 \
   │      ^^
+fail_escape.ml[1:6 ..1:7]: Use amc explain 0011 for more information
 fail_escape.ml[2:1 ..2:1]: error (E0004)
   Unexpected end of input, expecting `"` to close string
   │ 
 1 │ "\#  \0 \
   │ ^
 2 │ 
   │ ^
+fail_escape.ml[2:1 ..2:1]: Use amc explain 0004 for more information

tests/lexer/fail_unterminated_comment.out

@@ -5,3 +5,4 @@ fail_unterminated_comment.ml[7:1 ..7:1]: error (E0005)
   │ ^
 7 │ 
   │ ^
+fail_unterminated_comment.ml[7:1 ..7:1]: Use amc explain 0005 for more information

tests/lexer/fail_unterminated_string.out

@@ -3,10 +3,12 @@ fail_unterminated_string.ml[1:15 ..1:15]: error (E0004)
   │ 
 1 │ let x = "hello
   │         ^     ^
+fail_unterminated_string.ml[1:15 ..1:15]: Use amc explain 0004 for more information
 fail_unterminated_string.ml[2:1 ..2:1]: error (E0004)
   Unexpected end of input, expecting `"` to close string
   │ 
 1 │ let x = "hello
   │         ^
 2 │ 
   │ ^
+fail_unterminated_string.ml[2:1 ..2:1]: Use amc explain 0004 for more information

tests/parser/fail_bind_qualified.out

@@ -3,3 +3,4 @@ fail_bind_qualified.ml[1:6 ..1:14]: error (E0010)
   │ 
 1 │ let (`Foo.bar`) = ()
   │      ^^^^^^^^^
+fail_bind_qualified.ml[1:6 ..1:14]: Use amc explain 0010 for more information

tests/parser/fail_do_with.out

@@ -4,3 +4,4 @@ fail_do_with.ml[1:10 ..1:20]: error (E0009)
   │ 
 1 │ let () = with x <- 0
   │          ^^^^^^^^^^^
+fail_do_with.ml[1:10 ..1:20]: Use amc explain 0009 for more information

tests/parser/fail_malformed_class_name.out

@@ -3,6 +3,7 @@ fail_malformed_class_name.ml[1:7 ..1:12]: error (E0007)
   │ 
 1 │ class a -> b begin end
   │       ^^^^^^
+fail_malformed_class_name.ml[1:7 ..1:12]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[3:7 ..3:9]: error (E0007)
   Malformed class declaration beginning with X
 
@@ -12,6 +13,7 @@ fail_malformed_class_name.ml[3:7 ..3:9]: error (E0007)
   │ 
 3 │ class X a begin end
   │       ^^^
+fail_malformed_class_name.ml[3:7 ..3:9]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[4:7 ..4:11]: error (E0007)
   Malformed class declaration beginning with X
 
@@ -22,6 +24,7 @@ fail_malformed_class_name.ml[4:7 ..4:11]: error (E0007)
   │ 
 4 │ class X a b begin end
   │       ^^^^^
+fail_malformed_class_name.ml[4:7 ..4:11]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[6:7 ..6:9]: error (E0007)
   Malformed class declaration for x
 
@@ -31,6 +34,7 @@ fail_malformed_class_name.ml[6:7 ..6:9]: error (E0007)
   │ 
 6 │ class x a  begin end
   │       ^^^
+fail_malformed_class_name.ml[6:7 ..6:9]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[7:7 ..7:11]: error (E0007)
   Malformed class declaration for x
 
@@ -40,3 +44,4 @@ fail_malformed_class_name.ml[7:7 ..7:11]: error (E0007)
   │ 
 7 │ class x a b  begin end
   │       ^^^^^
+fail_malformed_class_name.ml[7:7 ..7:11]: Use amc explain 0007 for more information

tests/parser/fail_malformed_instance.out

@@ -3,3 +3,4 @@ fail_malformed_instance.ml[1:10 ..1:11]: error (E0008)
   │ 
 1 │ instance 'a begin end
   │          ^^
+fail_malformed_instance.ml[1:10 ..1:11]: Use amc explain 0008 for more information

tests/resolve/fail_import_abandon.out

@@ -5,17 +5,20 @@ fail_import_abandon.ml[6:8 ..6:30]: error (E1010)
   │ 
 6 │   open import "./not_found.ml"
   │        ^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_abandon.ml[6:8 ..6:30]: Use amc explain 1010 for more information
 fail_import_abandon.ml[15:17 ..15:39]: error (E1010)
   Cannot resolve "./not_found.ml"
 
   Arising from use of the module
    │ 
 15 │ module B = open import "./not_found.ml"
    │                 ^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_abandon.ml[15:17 ..15:39]: Use amc explain 1010 for more information
 fail_import_abandon.ml[25:12 ..25:22]: error (E1001)
   Variable not in scope: `not_defined`
 
   Arising from use of the expression
    │ 
 25 │   let () = not_defined
    │            ^^^^^^^^^^^
+fail_import_abandon.ml[25:12 ..25:22]: Use amc explain 1001 for more information

tests/resolve/fail_import_loop.out

@@ -14,3 +14,4 @@ tests/resolve/modules/loop_3.ml[1:12 ..1:31]: error (E1011)
 1 │ module M = import "./loop_2.ml"
   │            ^^^^^^^^^^^^^^^^^^^^
   • Note: "tests/resolve/modules/loop_2.ml" imported from "tests/resolve/modules/loop_1.ml"
+tests/resolve/modules/loop_3.ml[1:12 ..1:31]: Use amc explain 1011 for more information

tests/resolve/fail_import_not_found.out

@@ -5,3 +5,4 @@ fail_import_not_found.ml[1:6 ..1:36]: error (E1010)
   │ 
 1 │ open import "./modules/not_found.ml"
   │      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_not_found.ml[1:6 ..1:36]: Use amc explain 1010 for more information

tests/resolve/fail_import_not_found_path.out

@@ -5,3 +5,4 @@ fail_import_not_found_path.ml[1:6 ..1:26]: error (E1010)
   │ 
 1 │ open import "not_found.ml"
   │      ^^^^^^^^^^^^^^^^^^^^^
+fail_import_not_found_path.ml[1:6 ..1:26]: Use amc explain 1010 for more information

tests/resolve/fail_let_ambiguity.out

@@ -5,3 +5,4 @@ fail_let_ambiguity.ml[8:18 ..8:18]: error (E1002)
   │ 
 8 │ let main _ = x + y
   │                  ^
+fail_let_ambiguity.ml[8:18 ..8:18]: Use amc explain 1002 for more information

tests/resolve/fail_let_open_struct.out

@@ -5,3 +5,4 @@ fail_let_open_struct.ml[2:3 ..2:33]: error (E1009)
   │ 
 2 │   let open begin type t end in ()
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_let_open_struct.ml[2:3 ..2:33]: Use amc explain 1009 for more information

tests/resolve/fail_modules.out

@@ -5,3 +5,4 @@ fail_modules.ml[4:9 ..4:9]: error (E1001)
   │ 
 4 │ let y = x
   │         ^
+fail_modules.ml[4:9 ..4:9]: Use amc explain 1001 for more information

tests/resolve/fail_non_linear_record.out

@@ -4,3 +4,4 @@ fail_non_linear_record.ml[2:3 ..4:10]: error (E1004)
   │ 
 2 │   { x = 0,
   │   ^^^^^^^^
+fail_non_linear_record.ml[2:3 ..4:10]: Use amc explain 1004 for more information

tests/resolve/fail_pattern_ambiguity.out

@@ -5,17 +5,20 @@ fail_pattern_ambiguity.ml[4:3 ..4:8]: error (E1003)
   │ 
 4 │ | (a, a) -> a + a
   │    ^  ^
+fail_pattern_ambiguity.ml[4:3 ..4:8]: Use amc explain 1003 for more information
 fail_pattern_ambiguity.ml[4:13 ..4:13]: error (E1002)
   Ambiguous reference to variable: `a`
 
   Arising from use of the expression
   │ 
 4 │ | (a, a) -> a + a
   │             ^
+fail_pattern_ambiguity.ml[4:13 ..4:13]: Use amc explain 1002 for more information
 fail_pattern_ambiguity.ml[4:17 ..4:17]: error (E1002)
   Ambiguous reference to variable: `a`
 
   Arising from use of the expression
   │ 
 4 │ | (a, a) -> a + a
   │                 ^
+fail_pattern_ambiguity.ml[4:17 ..4:17]: Use amc explain 1002 for more information