24 KiB
Basics
non-exhaustive patterns
unique type T = A | B | C
test : T -> ()
test = cases
A -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
4 | test = cases
5 | A -> ()
Patterns not matched:
* B
* C
unique type T = A | B
test : (T, Optional T) -> ()
test = cases
(A, Some _) -> ()
(A, None) -> ()
(B, Some A) -> ()
(B, None) -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
4 | test = cases
5 | (A, Some _) -> ()
6 | (A, None) -> ()
7 | (B, Some A) -> ()
8 | (B, None) -> ()
Patterns not matched:
* (B, Some B)
redundant patterns
unique type T = A | B | C
test : T -> ()
test = cases
A -> ()
B -> ()
C -> ()
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
8 | _ -> ()
unique type T = A | B
test : (T, Optional T) -> ()
test = cases
(A, Some _) -> ()
(A, None) -> ()
(B, Some _) -> ()
(B, None) -> ()
(A, Some A) -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
9 | (A, Some A) -> ()
Uninhabited patterns
match is complete without covering uninhabited patterns
unique type V =
test : Optional (Optional V) -> ()
test = cases
None -> ()
Some None -> ()
Loading changes detected in scratch.u.
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 V
test : Optional (Optional V) -> ()
uninhabited patterns are reported as redundant
unique type V =
test0 : V -> ()
test0 = cases
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
5 | _ -> ()
unique type V =
test : Optional (Optional V) -> ()
test = cases
None -> ()
Some None -> ()
Some _ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
7 | Some _ -> ()
Guards
Incomplete patterns due to guards should be reported
test : () -> ()
test = cases
() | false -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | () | false -> ()
Patterns not matched:
* ()
test : Optional Nat -> Nat
test = cases
None -> 0
Some x
| isEven x -> x
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | None -> 0
4 | Some x
5 | | isEven x -> x
Patterns not matched:
* Some _
Complete patterns with guards should be accepted
test : Optional Nat -> Nat
test = cases
None -> 0
Some x
| isEven x -> x
| otherwise -> 0
Loading changes detected in scratch.u.
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`:
test : Optional Nat -> Nat
Pattern instantiation depth
Uncovered patterns are only instantiated as deeply as necessary to distinguish them from existing patterns.
unique type T = A | B | C
test : Optional (Optional T) -> ()
test = cases
None -> ()
Some None -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
4 | test = cases
5 | None -> ()
6 | Some None -> ()
Patterns not matched:
* Some (Some _)
unique type T = A | B | C
test : Optional (Optional T) -> ()
test = cases
None -> ()
Some None -> ()
Some (Some A) -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
4 | test = cases
5 | None -> ()
6 | Some None -> ()
7 | Some (Some A) -> ()
Patterns not matched:
* Some (Some B)
* Some (Some C)
Literals
Non-exhaustive
Nat
test : Nat -> ()
test = cases
0 -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | 0 -> ()
Patterns not matched:
* _
Boolean
test : Boolean -> ()
test = cases
true -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | true -> ()
Patterns not matched:
* false
Exhaustive
Nat
test : Nat -> ()
test = cases
0 -> ()
_ -> ()
Loading changes detected in scratch.u.
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`:
test : Nat -> ()
Boolean
test : Boolean -> ()
test = cases
true -> ()
false -> ()
Loading changes detected in scratch.u.
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`:
test : Boolean -> ()
Redundant
Nat
test : Nat -> ()
test = cases
0 -> ()
0 -> ()
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
4 | 0 -> ()
Boolean
test : Boolean -> ()
test = cases
true -> ()
false -> ()
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
5 | _ -> ()
Sequences
Exhaustive
test : [()] -> ()
test = cases
[] -> ()
x +: xs -> ()
Loading changes detected in scratch.u.
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`:
test : [()] -> ()
Non-exhaustive
test : [()] -> ()
test = cases
[] -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | [] -> ()
Patterns not matched:
* (() +: _)
test : [()] -> ()
test = cases
x +: xs -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | x +: xs -> ()
Patterns not matched:
* []
test : [()] -> ()
test = cases
xs :+ x -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | xs :+ x -> ()
Patterns not matched:
* []
test : [()] -> ()
test = cases
x0 +: (x1 +: xs) -> ()
[] -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | x0 +: (x1 +: xs) -> ()
4 | [] -> ()
Patterns not matched:
* (() +: [])
test : [()] -> ()
test = cases
[] -> ()
x0 +: [] -> ()
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
2 | test = cases
3 | [] -> ()
4 | x0 +: [] -> ()
Patterns not matched:
* (() +: (() +: _))
Uninhabited
Cons
is not expected since V
is uninhabited
unique type V =
test : [V] -> ()
test = cases
[] -> ()
Loading changes detected in scratch.u.
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 V
test : [V] -> ()
Length restrictions can equate cons and nil patterns
Here the first pattern matches lists of length two or greater, the
second pattern matches lists of length 0. The third case matches when the
final element is false
, while the fourth pattern matches when the
first element is true
. However, the only possible list length at
the third or fourth clause is 1, so the first and final element must
be equal. Thus, the pattern match is exhaustive.
test : [Boolean] -> ()
test = cases
[a, b] ++ xs -> ()
[] -> ()
xs :+ false -> ()
true +: xs -> ()
Loading changes detected in scratch.u.
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`:
test : [Boolean] -> ()
This is the same idea as above but shows that fourth match is redundant.
test : [Boolean] -> ()
test = cases
[a, b] ++ xs -> ()
[] -> ()
xs :+ true -> ()
true +: xs -> ()
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
6 | true +: xs -> ()
This is another similar example. The first pattern matches lists of
length 5 or greater. The second matches lists of length 4 or greater where the
first and third element are true. The third matches lists of length 4
or greater where the final 4 elements are true, false, true, false
.
The list must be exactly of length 4 to arrive at the second or third
clause, so the third pattern is redundant.
test : [Boolean] -> ()
test = cases
[a, b, c, d, f] ++ xs -> ()
[true, _, true, _] ++ _ -> ()
_ ++ [true, false, true, false] -> ()
_ -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
5 | _ ++ [true, false, true, false] -> ()
bugfix: Sufficient data decl map
unique type T = A
unit2t : Unit -> T
unit2t = cases
() -> A
Loading changes detected in scratch.u.
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 T
unit2t : 'T
.> add
⍟ I've added these definitions:
unique type T
unit2t : 'T
Pattern coverage checking needs the data decl map to contain all transitive type dependencies of the scrutinee type. We do this before typechecking begins in a roundabout way: fetching all transitive type dependencies of references that appear in the expression.
This test ensures that we have fetched the T
type although there is
no data decl reference to T
in witht
.
witht : Unit
witht = match unit2t () with
x -> ()
Loading changes detected in scratch.u.
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`:
witht : ()
unique type V =
evil : Unit -> V
evil = bug ""
Loading changes detected in scratch.u.
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 V
evil : 'V
.> add
⍟ I've added these definitions:
unique type V
evil : 'V
withV : Unit
withV = match evil () with
x -> ()
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
3 | x -> ()
unique type SomeType = A
Loading changes detected in scratch.u.
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 SomeType
.> add
⍟ I've added these definitions:
unique type SomeType
unique type R = R SomeType
get x = match x with
R y -> y
Loading changes detected in scratch.u.
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 R
get : R -> SomeType
unique type R = { someType : SomeType }
Loading changes detected in scratch.u.
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 R
R.someType : R -> SomeType
R.someType.modify : (SomeType ->{g} SomeType) -> R ->{g} R
R.someType.set : SomeType -> R -> R
Ability handlers
Exhaustive ability handlers are accepted
structural ability Abort where
abort : {Abort} a
result : '{e, Abort} a -> {e} a
result f = handle !f with cases
{ x } -> x
{ abort -> _ } -> bug "aborted"
Loading changes detected in scratch.u.
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`:
structural ability Abort
result : '{e, Abort} a ->{e} a
structural ability Abort where
abort : {Abort} a
unique type T = A | B
result : '{e, Abort} T -> {e} ()
result f = handle !f with cases
{ A } -> ()
{ B } -> ()
{ abort -> _ } -> bug "aborted"
Loading changes detected in scratch.u.
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`:
structural ability Abort
result : '{e, Abort} T ->{e} ()
⍟ These names already exist. You can `update` them to your
new definition:
unique type T
structural ability Abort where
abort : {Abort} a
result : '{e, Abort} V -> {e} V
result f =
impl : Request {Abort} V -> V
impl = cases
{ abort -> _ } -> bug "aborted"
handle !f with impl
Loading changes detected in scratch.u.
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`:
structural ability Abort
result : '{e, Abort} V ->{e} V
structural ability Abort where
abort : {Abort} a
structural ability Stream a where
emit : a -> {Stream a} Unit
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
handleMulti c =
impl xs = cases
{ r } -> (Some r, xs)
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
{ abort -> _ } -> (None, xs)
handle !c with impl []
Loading changes detected in scratch.u.
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`:
structural ability Abort
structural ability Stream a
handleMulti : '{Abort, Stream a} r -> (Optional r, [a])
Non-exhaustive ability handlers are rejected
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e} a
result f = handle !f with cases
{ abort -> _ } -> bug "aborted"
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
7 | result f = handle !f with cases
8 | { abort -> _ } -> bug "aborted"
Patterns not matched:
* { _ }
* { abortWithMessage _ -> _ }
structural ability Abort where
abort : {Abort} a
unique type T = A | B
result : '{e, Abort} T -> {e} ()
result f = handle !f with cases
{ A } -> ()
{ abort -> _ } -> bug "aborted"
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
7 | result f = handle !f with cases
8 | { A } -> ()
9 | { abort -> _ } -> bug "aborted"
Patterns not matched:
* { B }
unique ability Give a where
give : a -> {Give a} Unit
unique type T = A | B
result : '{e, Give T} r -> {e} r
result f = handle !f with cases
{ x } -> x
{ give A -> resume } -> result resume
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
7 | result f = handle !f with cases
8 | { x } -> x
9 | { give A -> resume } -> result resume
Patterns not matched:
* { give B -> _ }
structural ability Abort where
abort : {Abort} a
structural ability Stream a where
emit : a -> {Stream a} Unit
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
handleMulti c =
impl : [a] -> Request {Stream a, Abort} r -> (Optional r, [a])
impl xs = cases
{ r } -> (Some r, xs)
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
handle !c with impl []
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
10 | impl xs = cases
11 | { r } -> (Some r, xs)
12 | { emit x -> resume } -> handle !resume with impl (xs :+ x)
Patterns not matched:
* { abort -> _ }
Redundant handler cases are rejected
unique ability Give a where
give : a -> {Give a} Unit
unique type T = A | B
result : '{e, Give T} r -> {e} r
result f = handle !f with cases
{ x } -> x
{ give _ -> resume } -> result resume
{ give A -> resume } -> result resume
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
10 | { give A -> resume } -> result resume
Exhaustive ability reinterpretations are accepted
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e, Abort} a
result f = handle !f with cases
{ x } -> x
{ abort -> _ } -> abort
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
Loading changes detected in scratch.u.
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`:
structural ability Abort
result : '{e, Abort} a ->{e, Abort} a
structural ability Abort a where
abort : {Abort a} r
abortWithMessage : a -> {Abort a} r
result : '{e, Abort V} a -> {e, Abort V} a
result f =
impl : Request {Abort V} r -> {Abort V} r
impl = cases
{ x } -> x
{ abort -> _ } -> abort
handle !f with impl
Loading changes detected in scratch.u.
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`:
structural ability Abort a
result : '{e, Abort V} a ->{e, Abort V} a
Non-exhaustive ability reinterpretations are rejected
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e, Abort} a
result f = handle !f with cases
{ x } -> x
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
7 | result f = handle !f with cases
8 | { x } -> x
9 | { abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
Patterns not matched:
* { abort -> _ }
Hacky workaround for uninhabited abilities
Although all of the constructors of an ability might be uninhabited, the typechecker requires at least one be specified so that it can determine that the ability should be discharged. So, the default pattern match coverage checking behavior of prohibiting covering any of the cases is problematic. Instead, the pattern match coverage checker will require that at least one constructor be given, even if they are all uninhabited.
The messages here aren't the best, but I don't think uninhabited abilities will come up and get handlers written for them often.
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
handle !f with impl
Loading changes detected in scratch.u.
Pattern match doesn't cover all possible cases:
8 | impl = cases
9 | { x } -> x
Patterns not matched:
* { give _ -> _ }
* { give2 _ -> _ }
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give _ -> resume } -> bug "impossible"
handle !f with impl
Loading changes detected in scratch.u.
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 ability Give a
result : '{e, Give V} r ->{e} r
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give2 _ -> resume } -> bug "impossible"
handle !f with impl
Loading changes detected in scratch.u.
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 ability Give a
result : '{e, Give V} r ->{e} r
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give _ -> resume } -> bug "impossible"
{ give2 _ -> resume } -> bug "impossible"
handle !f with impl
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
11 | { give2 _ -> resume } -> bug "impossible"
unique ability GiveA a where
giveA : a -> {GiveA a} Unit
giveA2 : a -> {GiveA a} Unit
unique ability GiveB a where
giveB : a -> {GiveB a} Unit
giveB2 : a -> {GiveB a} Unit
result : '{e, GiveA V, GiveB V} r -> {e} r
result f =
impl : Request {GiveA V, GiveB V} r -> {} r
impl = cases
{ x } -> x
{ giveA _ -> _ } -> bug "impossible"
{ giveA2 _ -> _ } -> bug "impossible"
{ giveB _ -> _ } -> bug "impossible"
{ giveB2 _ -> _ } -> bug "impossible"
handle !f with impl
Loading changes detected in scratch.u.
This case would be ignored because it's already covered by the preceding case(s):
15 | { giveA2 _ -> _ } -> bug "impossible"
unique ability GiveA a where
giveA : a -> {GiveA a} Unit
giveA2 : a -> {GiveA a} Unit
unique ability GiveB a where
giveB : a -> {GiveB a} Unit
giveB2 : a -> {GiveB a} Unit
result : '{e, GiveA V, GiveB V} r -> {e} r
result f =
impl : Request {GiveA V, GiveB V} r -> {} r
impl = cases
{ x } -> x
{ giveA2 _ -> _ } -> bug "impossible"
{ giveB _ -> _ } -> bug "impossible"
handle !f with impl
Loading changes detected in scratch.u.
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 ability GiveA a
unique ability GiveB a
result : '{e, GiveA V, GiveB V} r ->{e} r