How to properly handle Fin n and Integer when computing dates?

In my journey exploring Idris, I am trying to write a small dates-handling module in an "idiomatic" way. Here is what I have so far.

First I have some basic types to represent days, months and years:

module Date 

import Data.Fin

Day : Type
Day = Fin 32

data Month : Type where
  January    : Month
  February   : Month
  .... 

toNat : Month -> Nat
toNat January    = 1
toNat February   = 2
... 

data Year : Type where
  Y : Integer -> Year

record Date where
  constructor MkDate
  day   : Day
  month : Month 
  year  : Year

I would like to implement a function addDays to add some number of days to a Date. To this end I defined the following auxiliary functions:

isLeapYear : Year -> Bool
isLeapYear (Y y) = 
  (((y `mod` 4) == 0) && ((y `mod` 100) /= 0)) || ((y `mod` 400) == 0) 

daysInMonth : Month -> Year -> Day
daysInMonth January _      = 31
daysInMonth February year  = if isLeapYear year then 29 else 28
daysInMonth March _        = 31
...

And finally try to define addDays as :

addDays : Date -> Integer -> Date
addDays (MkDate d m y) days =
  let maxDays = daysInMonth m y
      shiftedDays = finToInteger d + days
  in case integerToFin shiftedDays (finToNat maxDays) of  
          Nothing => ?hole_1
          Just x  => MkDate x m y

I am stuck with the very basic case where the added number of days fit in the current month's duration. Here is the output of compiler:

When checking right hand side of Date.case block in addDays at Date.idr:92:11 with expected type Date

 When checking argument day to constructor Date.MkDate:
         Type mismatch between
                 Fin (finToNat maxDays) (Type of x)
         and
                 Day (Expected type)

         Specifically:
                 Type mismatch between
                         finToNat maxDays
                 and
                         32

This is puzzling because the type of maxDays should be obviously Day which is simply Fin 32.

I suspect this might be related to non-totality of daysInMonth which stems from non-totality of isLeapYear which itself comes from non-totality of mod for Integer type.

Solution

Well, this is not so trivial because Idris requires proofs from you on every step especially if you're using dependent types. All basic ideas are already written in this question:

Is there a way to define a consistent date in a dependent type language?

I'll comment your implementation and translate code in answer (it's probably Agda) to Idris. Also I made few adjustments to make your code total.

First, Month can be written a little bit simpler:

data Month = January
           | February
           | March

I'm not going to write all 12 month, it's just an example.

Second, Year type should store Nat instead of Integer because most functions that work with Integer aren't total. This is better:

data Year : Type where
    Y : Nat -> Year

It helps to make isLeapYear check total:

isLeapYear : Year -> Bool
isLeapYear (Y y) = check4 && check100 || check400
  where
    check4 : Bool
    check4 = modNatNZ y 4 SIsNotZ == 0

    check100 : Bool
    check100 = modNatNZ y 100 SIsNotZ /= 0

    check400 : Bool
    check400 = modNatNZ y 400 SIsNotZ == 0

Next, it's not good to make Day as a Fin 32. Better to specify day's number for each month specifically.

daysInMonth : Month -> Year -> Nat
daysInMonth January  _    = 31
daysInMonth February year = if isLeapYear year then 29 else 28
daysInMonth March    _    = 31

Day : Month -> Year -> Type
Day m y = Fin (daysInMonth m y)

And you should adjust a little your Date record:

record Date where
    constructor MkDate
    year  : Year
    month : Month
    day   : Day month year

Well, now about addDays. This function is actually very complex when you're working with dependent types. As you correctly noticed, you have several cases. For example: sum fits in the current month, sum goes to next month, sum skips several months, sum goes to year. And each such case need proof. If you want to ensure that sum fits in current month, you should provide a proof of that fact.

Before I move to code I want to warn you that writing even non-typed versions of date library is increadibly hard. Moreover, I suppose nobody haven't still tried to implement full-featured version in some language with dependent types. So my solution may be far from the best. But at least should give you some ideas about what you're doing wrong.

Then you can start with writing some function like this:

daysMax : (d: Date) -> Nat
daysMax (MkDate y m _) = daysInMonth m y

addDaysSameMonth : (d : Date)
                -> (n : Nat)
                -> Prelude.Nat.LT (finToNat (day d) + n) (daysMax d)
                -> Date
addDaysSameMonth d n x = ?addDaysSameMonth_rhs

Well, numeric operations with Fin are very limited according to current state of Data.Fin module. So you may have hard times even adding two Nats and converting them to Fin using given proof. Again, writing such stuff is harder than it seems :)

Here is the full sketch of code: http://lpaste.net/3314444314070745088