Idris unit tests using the type checker

test.idr

{-
  From the Prelude: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Bool.idr#L18-L27
  data so : Bool -> Type where oh : so True
-}

-- Type checks fine
passTest : so (1 < 2)
passTest = oh

-- Fails to type check
failTest : so (2 < 1)
failTest = oh

{-
  Type checking ./test.idr
  test.idr:5:12:When elaborating right hand side of failTest:
  Can't unify
          so True
  with
          so False
  
  Specifically:
          Can't unify
                  True
          with
                  False
-}