Injectivity annotations and overlap

Learn
#1

I’ve recently been using the package nonempty-containers (and writing — heaven forbid — orphan instances) to better wield the type-level guarantees about the data structures I use. The HasNonEmpty type class gives you the power to “ignore” the empty case within your program — or at least to specify it in its own place. However to do so, the programmer must specify the type NE x for whatever container type x may be. My next thought was to implement the class for Maybe x — after all, NE (Maybe x) is just x, right?

{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Maybe' where

import Data.Containers.NonEmpty (HasNonEmpty (..))
import Data.Functor.Identity (Identity (..))

instance HasNonEmpty (Maybe x) where
  type NE (Maybe x) = x
  -- gives me the following errors:

-- Type family equation right-hand sides overlap; this violates
-- the family's injectivity annotation:
--   NE [a] = GHC.Base.NonEmpty a
--     -- Defined in module Data.Containers.NonEmpty
--   NE (Maybe x) = x
--     -- Defined at /Users/mbrown/Documents/Code/Haskell/list1/lib/Data/Maybe'.hs:14:8

-- Type family equation violates the family's injectivity annotation.
-- RHS of injective type family equation is a bare type variable
-- but these LHS type and kind patterns are not bare variables: ‘Maybe
--                                                                 x’
--   NE (Maybe x) = x
--     -- Defined at /Users/mbrown/Documents/Code/Haskell/list1/lib/Data/Maybe'.hs:14:8

Instead, to make this work, I have to write

instance HasNonEmpty (Maybe x) where
  type NE (Maybe x) = Identity x
  nonEmpty = fmap Identity
  empty = Nothing
  fromNonEmpty = Just . runIdentity

and then using this abstraction remains clumsy because of the extra Identity.

What makes the first type equation non-injective? Does this have anything to do with the least fixed-point functor?

#2

The first is non-injective because if you have [Int], should the NE type be NonEmpty Int or Maybe [Int]?

#3

type NE (Maybe [Int]) = [Int]
type NE [Int] = NonEmpty Int

#4

The first is non-injective because if NE t = NonEmpty a then should I infer t to be [a] or Maybe (NonEmpty a)?

2 Likes
#5

Ah, I understand! The ambiguity comes from the type checking, when the compiler comes across a use of (a method of) HasNonEmpty for a type it has not unified. Using Identity allows the unification to be deferred, because the type variable does not escape its context.