[GHC] #16266: Allow definition of functions with absurd contexts

1 Feb 2019

      #16266: Allow definition of functions with absurd contexts
-------------------------------------+-------------------------------------
           Reporter:  So8res         |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  low            |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following code:

 {{{#!hs
 {-# 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).

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16266
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler