Idris datatype invariant

Invariant.idr

module Main

import Data.String 

data CorrectSize : Nat -> Nat -> Nat -> Type where
  SmallerThan150 : (x : Nat) -> (y : Nat) -> (z : Nat) -> {auto prf : x + y + z <= 150 = True} -> CorrectSize x y z

Show (CorrectSize x y z) where
  show (SmallerThan150 x y z) = "CorrectSize " ++ show (x, y, z)
  showPrec _ size = show size
  
mkCorrectSize : (x : Nat) -> (y : Nat) -> (z : Nat) -> Maybe (CorrectSize x y z)
mkCorrectSize x y z =
  case decEq (x + y + z <= 150) True of
    Yes prf => Just (SmallerThan150 x y z)
    No      => Nothing

main : IO ()
main = do
  Just dynX <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "X is not a number"
  Just dynY <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Y is not a number"
  Just dynZ <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Z is not a number"
  let static1 = SmallerThan150 120 20 10 -- Ok, value is known at compile time
  let static2 = SmallerThan150 50 90 10 -- Ok, value is known at compile time
  let static3 = SmallerThan150 50 50 50 -- Ok, value is known at compile time
  -- let static4 = SmallerThan150 120 120 10 -- Not ok, doesn't compile, value is known at compile time
  -- let static5 = SmallerThan150 80 80 50 -- Not ok, doesn't compile value is known at compile time
  let correctOrNothing = mkCorrectSize dynX dynY dynZ -- Ok if dynamic data is ok, value is checked by smart constructor
  -- let surelyCorrect = SmallerThan150 dynX dynY dynZ -- Not ok, doesn't compile
  putStrLn (show correctOrNothing)
  pure ()

SoInvariant.idr

-- Alternative version with `So`
module Main

import Data.String 
import Data.So

data CorrectSize : Nat -> Nat -> Nat -> Type where
  SmallerThan150 : (x : Nat) -> (y : Nat) -> (z : Nat) -> {auto prf : So (x + y + z <= 150)} -> CorrectSize x y z

Show (CorrectSize x y z) where
  show (SmallerThan150 x y z) = "CorrectSize " ++ show (x, y, z)
  showPrec _ size = show size
  
mkCorrectSize : (x : Nat) -> (y : Nat) -> (z : Nat) -> Maybe (CorrectSize x y z)
mkCorrectSize x y z =
  case choose (x + y + z <= 150) of
    Left oh => Just (SmallerThan150 x y z)
    _       => Nothing

main : IO ()
main = do
  Just dynX <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "X is not a number"
  Just dynY <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Y is not a number"
  Just dynZ <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Z is not a number"
  let static1 = SmallerThan150 120 20 10 -- Ok, value is known at compile time
  let static2 = SmallerThan150 50 90 10 -- Ok, value is known at compile time
  let static3 = SmallerThan150 50 50 50 -- Ok, value is known at compile time
  -- let static4 = SmallerThan150 120 120 10 -- Not ok, doesn't compile, value is known at compile time
  -- let static5 = SmallerThan150 80 80 50 -- Not ok, doesn't compile value is known at compile time
  let correctOrNothing = mkCorrectSize dynX dynY dynZ -- Ok if dynamic data is ok, value is checked by smart constructor
  -- let surelyCorrect = SmallerThan150 dynX dynY dynZ -- Not ok, doesn't compile
  putStrLn (show correctOrNothing)
  pure ()