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

changed weight to 3

added Tfeature request Trac import labels

added Plow label

Related: #15558 (comment 168315), while a bad diagnostic message that made that situation was fixed, and the ticket close, I also wanted something like this, and that part wasn't resolved, but @rae was thinking about what it might look like.

marked this issue as related to #15558 (closed)

OTOH #17295 (comment 226163) @simonpj originally thought that ticket was for what this one asks for, and wasn't keen on implementing it.

I think it's import to break down just where these absurdities come from. Regular classes, after all, are either "true" or "unknown", to keep type class reasoning monotonic, so we have the "open world" of instances it's always safe to extend. The two sources of real absurd constraints I know of are equivalence relations and partial closed families.

Absurdity with equivalence equivalence relations

~ and Coercible constarints however have their own special solver which has some support for real failure cases. This is OK because "instances" are automatic, and the open world of types doesn't prevent identifying inequalities. But this special support frequently annoys me as much as it helps. For example:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

witness :: a ~ b => a :~: b
witness = Refl

f :: Int ~ () => Int -> ()
f = case witness of {}

Can witness be inlined? I am not sure how.

On the other hand, I am fine accepting that I need to go from constraints (~) to regular types (:~:) to do the empty case, as long as I always can do that.

Absurdity from partial closed type families

Firstly, I'd thought I'd point that I'm with @rae and https://arxiv.org/pdf/1706.09715.pdf that we ought to disallow partial type families by making family applications with unmatched patterns a stuck term. In other words, Head '[] should be a compiler error, not just something that doesn't normalize. I think your IsList example could be implemented quite well with a closed type class, something like

class IsList xs where
  isList :: (xs ~ '[] => r) -> (forall h t. (xs ~ (h ': t)) => r) -> r
  instance IsList '[] where
    isList emptyCase _ = emptyCase
  instance IsList (x ': y) where
    isList _ consCase = consCase

As to what to do in the short term, hmmm. Maybe we can augment the equality relation solver thing to know that stuck terms stemming from closed type familes are not equal to anything else? e.g.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
import Data.Type.Equality

type family Partial (xxs :: [a]) where
  Partial (x ': xs) = x

witness :: a ~ b => a :~: b
witness = Refl

-- already OK
sillyExample0 :: (() ~ Int) => a -> b
sillyExample0 = case witness @() @Int of {}

-- proposed should be OK
sillyExample1 :: ('[] ~ Partial '[]) => a -> b
sillyExample1 = case witness @'[] @(Partial '[]) of {}

The idea is closed definitions need not be safe to extend, so we can allow partiality to be relied upon.

mentioned in merge request !2080 (closed)