Haskell: How to test that code isn't compiling?

Question

What is the best way to test that a declaration is not type-correct? With GADTs, it is not trivial to figure out that a constructor application is correct or not. If one is writing a library of type-safe constructs it is natural to ensure that illegal construct cannot be created. So, as a part of a test suite, I want to ensure that some example illegal constructs are rejected by the type checker.

As an example, see a size-checked Vector representation. It is much simpler than the typical problems I want to decide, but its a good example to check the testing method.

data Vector n t where
  EmptyVec :: Vector 0 t
  ConsVec  :: t -> Vector n t -> Vector (n+1) t

// TODO: test that it does not typecheck
illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec)

Answer 1

You can call GHCi from a Haskell program and use it to check strings. hint from hackage provides a convenient wrapper for this:

{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

import GHC.TypeLits
import Language.Haskell.Interpreter

data Vector n t where
    EmptyVec :: Vector 0 t
    ConsVec  :: t -> Vector n t -> Vector (n + 1) t 

main = do
    print =<< runInterpreter (typeChecks "ConsVec 'c' (ConsVec \"b\" EmptyVec)")
    -- prints "Right False"

Of course, this is just a more convenient alternative to writing scripts for checking text files, but I believe there isn't a way to reflect type checking itself in Haskell, so this is what we've got.

Answer 2

I got a different idea based on (ab?)using GHC's -fdefer-type-errors option instead, which might be cheaper than embedding a full Haskell interpreter like with hint. Its output is a bit messy though, because the warnings are still printed during compilation, but it can be cleaned up if you're willing to turn off warnings in general with the GHC -w option in both the file and on the ghc command line.

Although I include everything to demonstrate it in one module here, I assume the options for this test should only be properly enabled in the relevant test module.

Note that this method depends on being able to evaluate the offending value deeply enough to reveal its deferred type errors, which might be tricky in some use cases.

{-# OPTIONS_GHC -fdefer-type-errors #-}
{-# LANGUAGE TypeOperators, GADTs, DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.TypeLits
import Control.Exception
import Data.Typeable

data Vector n t where
  EmptyVec :: Vector 0 t
  ConsVec  :: t -> Vector n t -> Vector (n+1) t

-- Add a Show instance so we can evaluate a Vector deeply to catch any
-- embedded deferred type errors.
deriving instance Show t => Show (Vector n t)

illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec)

test = do
    t <- try . evaluate $ length (show illegalVec)
    case t of
        Right _ -> error "Showing illegalVec gave no error"
        Left e -> putStrLn $ "\nOk: Showing illegalVec returned error:\n"
                    ++ show (e :: ErrorCall)
-- ErrorCall is the exception type returned by the error function and seems
-- also to be used by deferred type errors.