Allow definition of functions with absurd contexts
Consider the following code:
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
type family Head xxs where
Head (x ': xs) = x
type family Tail xxs where
Tail (x ': xs) = xs
class IsList xs where
isList :: (xs ~ '[] => r) > ((xs ~ (Head xs ': Tail xs), IsList (Tail xs)) => r) > r
instance IsList '[] where isList r _ = r
instance IsList xs => IsList (x ': xs) where isList _ r = r
nonEmptyListsAreNotEmpty :: (xs ~ '[], xs ~ (Head xs ': Tail xs)) => r
nonEmptyListsAreNotEmpty = error "you convinced GHC that '[] ~ (_ ': _)!"
sillyExample :: forall x xs. IsList (x ': xs) => ()
sillyExample = isList @(x ': xs) nonEmptyListsAreNotEmpty ()
In this code, we define a class IsList which serves as a proof that something is a typelevel list, via the function isList. When using this, we may occasionally get into a situation where the types guarantee that we're working with a nonempty list, but we're asked to handle the emptylist case anyway. Suppose we want to define a nice little "absurd" function that serves as a reminder to readers that this code branch is impossible, in a way that GHC can verify. This function is named "nonEmptyListsAreNonEmpty" above.
Unfortunately, this code fails with
Main.hs:25:34: error:
• Couldn't match type ‘'[]’ with ‘Head '[] : Tail '[]’
arising from a use of ‘nonEmptyListsAreNotEmpty’
• In the second argument of ‘isList’, namely
‘nonEmptyListsAreNotEmpty’
In the expression: isList @(x : xs) nonEmptyListsAreNotEmpty ()
In an equation for ‘sillyExample’:
sillyExample = isList @(x : xs) nonEmptyListsAreNotEmpty ()

25  sillyExample = isList @(x ': xs) nonEmptyListsAreNotEmpty ()
 ^^^^^^^^^^^^^^^^^^^^^^^^
And indeed, the fact that [] can't be matched against (_ : _) is in some sense the point. More generally, whenever I'm fooling around with this sort of Haskell code (in which classes are being used to provide runtime witnesses of typelevel structure), I relatively regularly find myself in a branch of code where the context is obviously inconsistent, wishing that I had some way to say "search your heart, GHC; you know this case to be impossible". The fact that I can't even factor out this dead code into a function like nonEmptyListsAreNonEmpty just seems like insult added to injury.
This is a minor concern, to be sure. Nevertheless, it seems to me that we should be able to write this function somehow, especially given that there are various ways to trick GHC into accepting something analogous (by clever use of GADTs such as :~:, perhaps).
Trac metadata
Trac field  Value 

Version  8.6.3 
Type  FeatureRequest 
TypeOfFailure  OtherFailure 
Priority  low 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 