{"id":496,"date":"2022-08-30T15:02:19","date_gmt":"2022-08-30T15:02:19","guid":{"rendered":"https:\/\/unknownerror.org\/index.php\/2013\/11\/09\/gadts-failed-exhaustiveness-checking-collection-of-common-programming-errors\/"},"modified":"2022-08-30T15:02:19","modified_gmt":"2022-08-30T15:02:19","slug":"gadts-failed-exhaustiveness-checking-collection-of-common-programming-errors","status":"publish","type":"post","link":"https:\/\/unknownerror.org\/index.php\/2022\/08\/30\/gadts-failed-exhaustiveness-checking-collection-of-common-programming-errors\/","title":{"rendered":"GADT's failed exhaustiveness checking-Collection of common programming errors"},"content":{"rendered":"

The problem actually reported is:<\/p>\n

Warning: Pattern match(es) are non-exhaustive\n         In an equation for `fun': Patterns not matched: Inl _\n<\/code><\/pre>\n
Which is true. You provide a case for the Inr<\/code> constructor, but not the Inl<\/code> constructor.<\/p>\n
What you’re hoping is that since there’s no way to provide a value of type Sig B<\/code> that uses the Inl<\/code> constructor (it would need an argument of type Foo B<\/code>, but the only constructor for Foo<\/code> is of type Foo A<\/code>), that ghc will notice that you don’t need to handle the Inl<\/code> constructor.<\/p>\n
The trouble is that due to bottom every type is inhabited. There are<\/em> values of type Sig B<\/code> that use the Inl<\/code> constructor; there are even non-bottom values. They must contain<\/em> bottom, but they are not themselves bottom. So it is possible for the program to be evaluating a call to fun<\/code> that fails to match; that’s what ghc is warning about.<\/p>\n
So to fix that you need to change fun<\/code> to something like this:<\/p>\n
fun :: Sig B -> Int\nfun (Inr Bar) = 1\nfun (Inl foo) = error \"whoops\"\n<\/code><\/pre>\n
But now of course if you later add Baz :: Foo B<\/code> this function is a time bomb waiting to happen. It’s be nice for ghc to warn about that<\/em>, but the only way to make that happen is to pattern match foo<\/code> against a currently-exhaustive set of patterns. Unfortunately there are<\/em> no valid patterns you can put there! foo<\/code> is known to be of type Foo B<\/code>, which is only inhabited by bottom, and you can’t write a pattern for bottom.<\/p>\n
But you could pass it to a function that accepts an argument of polymorphic type Foo a<\/code>. That function could then match against all the currently-existing Foo<\/code> constructors, so that you’ll get a warning if you later add one. Something like this:<\/p>\n
fun :: Sig B -> Int\nfun (Inr Bar) = 1\nfun (Inl foo) = errorFoo foo\n    where \n        errorFoo :: Foo a -> b\n        errorFoo Foo = error \"whoops\"\n<\/code><\/pre>\n
Now You’ve properly handled all the constructors of :+:<\/code> in fun<\/code>, the “impossible” case simply errors out if it ever actually occurs and if you ever add Baz :: Foo B<\/code> you get a warning about a non-exhaustive pattern in errorFoo<\/code>, which is at least directing you to look at fun<\/code> because it’s defined in an attached where<\/code>.<\/p>\n
On the downside, when you add unrelated constructors to Foo<\/code> (say more of type Foo A<\/code>) you’ll have to add more cases to errorFoo<\/code>, and that could be unfun (though easy and mechanical) if you’ve got lots of functions applying this pattern.<\/p>\n
Originally posted 2013-11-09 19:46:24. <\/small><\/p>","protected":false},"excerpt":{"rendered":"
The problem actually reported is: Warning: Pattern match(es) are non-exhaustive In an equation for `fun’: Patterns not matched: Inl _ Which is true. You provide a case for the Inr constructor, but not the Inl constructor. What you’re hoping is that since there’s no way to provide a value of type Sig B that uses […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-496","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/posts\/496","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/comments?post=496"}],"version-history":[{"count":0,"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/posts\/496\/revisions"}],"wp:attachment":[{"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/media?parent=496"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/categories?post=496"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/unknownerror.org\/index.php\/wp-json\/wp\/v2\/tags?post=496"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}