Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What "Contraint is no smaller than the instance head" means and how to solve it

Tags:

haskell

I would like to write something like:

{-# LANGUAGE FlexibleContexts,FlexibleInstances #-}

import Data.ByteString.Char8 (ByteString,pack)
import Data.Foldable (Foldable)

class (Show a) => Rows a where
    rRepr :: a -> [ByteString]
    rRepr = (:[]) . pack . show

instance (Foldable f,Show (f a)) => Rows (f a) where
    rRepr = const []

meaning that f a instantiate Rows if f instantiate Foldable and f a instantiate Show. When I run ghc I get:

Constraint is no smaller than the instance head
  in the constraint: Show (f a)
(Use -XUndecidableInstances to permit this)
In the instance declaration for `Rows (f a)'

I have two questions:

  • what "smaller" means in the error and what is the problem?
  • what is the right way to define what I want without using UndecidableInstances?
like image 838
mariop Avatar asked Jul 25 '13 16:07

mariop


1 Answers

Let's play compiler: we have a type (f a) we'd like to see if it is a valid satisfier of a Rows constraint. To do so, we need to dispatch a proof that (f a) satisfies Show (f a) as well. This isn't a problem unless someone writes an

 instance Rows (f a) => Show (f a) where ...

in which case I'm back where I began. Encoding an infinite loop like this is sort of foolish, but Haskell statically ensures that it's actually impossible unless you ask for UndecidableInstances.


Normally Haskell ensures that each step of a "resolution chase" reduces the size of the type by at least 1 constructor. This leads to a really simple proof by structural induction that we'll end up with a bare type in a finite number of resolutions.

This is overly restrictive, clearly some instance resolution steps are meaningful, useful, and total even if they don't immediately reduce the constructor tree. This same kind of totality restriction applies in languages like Agda and Coq and often it's a bit of an illustrative challenge to manipulate your algorithm into one which proceeds by structural induction.


So how can we fix it? One way is to lose the Show constraint on the class definition use an instance like Show1 from prelude-extras.

class Show1 f where ...
show1 :: (Show1 f, Show a) => f a -> String  -- not an instance definition!

and then have instance (Foldable f, Show1 f, Show a) => Rows (f a) where ... which works in my testing. You can then write a default instance as a standalone function.

defRRepr :: Show a => a -> [ByteString]
defRRepr = (:[]) . pack . show

and use it whenever writing an instance definition for a Showable thing.


The other solution is to use newtype wrappers to allow Haskell to see that a "layer" of resolution has been removed.

instance (Foldable f, Show (f a)) => Rows (FoldableRow f a) where
    rRepr = const [] . unFR

newtype FoldableRow f a = FR { unFR :: f a } deriving (Show)
like image 129
J. Abrahamson Avatar answered Oct 11 '22 01:10

J. Abrahamson