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 type-level 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 non-empty list, but we're asked to handle the empty-list 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 type-level 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