#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