Fix up minor haskell issues.

Need to be careful about operations that are ambiguous in Haskell
but well-defined in the resulting Isabelle import.

haskell/src/SEL4/Kernel/VSpace/ARM.lhs

@@ -1093,9 +1093,7 @@ Capabilities for page directories --- the top level of the hardware-defined page
 >                 -- Fail if there is nothing mapped here
 >                 Nothing -> return $ InvokePageDirectory PageDirectoryNothing
 >                 Just frameInfo -> do
->                     withoutFailure $ stateAssert 
->                         (validMappingSize (fst frameInfo))
->                         "mapping found in PD is of invalid size"
+>                     withoutFailure $ checkValidMappingSize (fst frameInfo)
 >                     let baseStart = pageBase (VPtr start) (fst frameInfo)
 >                     let baseEnd = pageBase (VPtr end - 1) (fst frameInfo)
 >                     when (baseStart /= baseEnd) $
@@ -1313,8 +1311,8 @@ When we fetch a mapping in which to perform a page flush, we assert that its
 size is valid. This check is ignored in Haskell, but the Isabelle model has a
 notion of the largest permitted object size, and checks it appropriately.
 
-> validMappingSize :: VMPageSize -> KernelState -> Bool
-> validMappingSize _ = const True
+> checkValidMappingSize :: VMPageSize -> Kernel ()
+> checkValidMappingSize _ = return ()
 
 \subsection{Invocation Implementations}
 

haskell/src/SEL4/Object/TCB.lhs

@@ -587,7 +587,7 @@ When a new "Wait" operation begins, the caller slot in the waiting thread's TCB
 > deleteCallerCap receiver = do
 >     callerSlot <- getThreadCallerSlot receiver
 >     callerCap <- getSlotCap callerSlot
->     assert (isReplyCap callerCap || callerCap == NullCap)
+>     assert (isReplyCap callerCap || isNullCap callerCap)
 >         "Caller cap must be a reply cap"
 >     cteDeleteOne callerSlot