Debug: Couldn't match expected type ‘GHC.Types.Bool’ with actual type ‘Bool’

Question

I'm trying to resolve the following exercise of Haskell:

Define the function exists::(N-> Bool)-> N->Bool, which receives a predicate p and a natural n, and returns True if there is any number between O and n for which p is true. Examples:

exists pair three = True
exists isGreaterThanZero O = False

This code goes before of my exists function:

{-#LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}

module Naturales where

import Prelude(Show)

data Bool where {   False :: Bool; 
                    True :: Bool
                } deriving Show

{- Data Type of Natural Numbers -}
data N where { O :: N ; 
               S :: N -> N 
            } deriving Show
    
    zero:: N
    zero= O
    
    one:: N
    one = S O
    
    two :: N
    two = S one 
    
    three :: N
    three = S two 
    
    four :: N
    four = S three
    ...

This is how I programmed the requested function called exists but when i try to compile the .hs code it says

exists:: (N->Bool)->N->Bool
exists = \p -> \x -> case x of {
            O -> p O;
            (S y) -> if p (S y) then True else existe p y; {- Line 288 -}
        }


    • Couldn't match expected type ‘GHC.Types.Bool’
                  with actual type ‘Bool’
      NB: ‘Bool’ is defined at EstudiandoRecursion.hs:(9,1)-(11,47)
          ‘GHC.Types.Bool’
            is defined in ‘GHC.Types’ in package ‘ghc-prim-0.5.3’
    • In the expression: p (S y)
      In the expression: if p (S y) then True else existe p y
      In a case alternative:
          (S y) -> if p (S y) then True else existe p y
    |
288 |                         (S y) -> if p (S y) then True else existe p y;     | 

I suppose that the logic of my function exists it's correct, but perhaps I have made syntax error writing the code.

Answer 1

You have redefined the standard Bool type. Haskell does not know that your own redefined type is actually the same as the standard one, so it treats them as two separate types: Bool (yours), and GHC.Types.Bool (the standard one).

The if cond then t else e expression only works with the standard Bool type, not your custom one. Hence, you can't use it in

if p (S y) then True else exists p y

since p (S y) returns your own custom Bool. Consider instead

case p (S y) of
   True  -> True
   False -> exists p y

which, unlike if, should work, picking the right True and False constructors from you new type. You can use case .. of { .. ; ... } if you prefer braces and semicolons.

Answer 2

You are making use of a if … then … else … expression. This requires the condition to be of type Bool, and this is the builtin Bool, so defining your own Bool type will not suffice.

It is however sufficient to work with a case … of … clause and thus pattern match on your True/False data constructors:

exists:: (N -> Bool) -> N -> Bool
exists = \p -> \x -> case x of {
            O -> p O;
            (S y) -> case p (S y) of
                True -> True
                _ -> exists p y
        }