Haskell: How to verify that code is not compiling?

Question

What is the best way to verify that the declaration does not match the correct type? With GADT, it’s not trivial that a constructor application is right or wrong. If you are writing a library such as safe constructs, it is natural that you cannot create an illegal construct. So, as part of the test suite, I want some examples of illegal constructs to be rejected using type checking.

For an example, see a size-dependent vector representation. This is much simpler than the typical problems I want to solve, but it is a good example to test the testing method.

data Vector nt where EmptyVec :: Vector 0 t ConsVec :: t -> Vector nt -> Vector (n+1) t // TODO: test that it does not typecheck illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec) 

Answer 1

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

 {-# LANGUAGE DataKinds, TypeOperators, GADTs #-} import GHC.TypeLits import Language.Haskell.Interpreter data Vector nt where EmptyVec :: Vector 0 t ConsVec :: t -> Vector nt -> 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 to check text files, but I believe that in Haskell there is no way to reflect type checking, so this is what we have.

Answer 2

I got another idea based on (ab?) Using the GHC -fdefer-type-errors option, which may be cheaper than implementing a full Haskell interpreter, for example using hint . Its output is a bit messy because warnings are still printed at compile time, but you can clear it if you want to disable warnings in general using the GHC -w option in both the file and the ghc command line.

Although I am including everything to demonstrate this in one module here, I believe that the parameters of this test should be correctly included in the corresponding test module.

Please note that this method depends on how capable it is to sufficiently deeply assess the value of the violation in order to identify deferred errors that can be difficult in some cases.

 {-# OPTIONS_GHC -fdefer-type-errors #-} {-# LANGUAGE TypeOperators, GADTs, DataKinds #-} {-# LANGUAGE StandaloneDeriving #-} import GHC.TypeLits import Control.Exception import Data.Typeable data Vector nt where EmptyVec :: Vector 0 t ConsVec :: t -> Vector nt -> 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 nt) 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.