Case expression in dependent type not working as expected in Idris

Question

I am playing around porting small bits of PureScript code to Idris where dependent types could be applied and stumbled across a situation where using case inside a dependent type is not working.

Since this is valid (simplified):

data ValidInvoice3 : (ft : FeeType) -> Type where
  MkVI3 : ValidInvoice3 ft

why does the following not type check?

-- BROKEN
data ValidInvoice4 : (ft : FeeType) -> Type where
  MkVI4 : case ft of
            FeeMarkupHidden => ValidInvoice4 ft -- simplified;
            FeeExplicit     => ValidInvoice4 ft -- more elaborate example below

In case you are interested why I am looking into this: here a bit more elaborate sample code:

module DependentWithCase

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
  MkFee : Fee ft -- simplified

data ValidArticle : (ft : FeeType) -> Type where
  MkVA : ValidArticle ft -- simplified

Here now is how the dependent type for “invoice” can be written successfully, indexed on FeeType, using a case expression to decide if a fee is added as an explicit parameter (in the actual code, in this case, the “article” type then has a “markup” part, which I have left out here; this way I can be sure the “markup” is only invoiced once):

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft ->
         case ft of FeeMarkupHidden => Unit; FeeExplicit => Fee ft;
         ->
         ValidInvoice ft

So you see the invoice data type (and in the actual code, the article type too) depends on the fee type.

But instead of using a case expression buried inside the constructor, I would much rather have it look like this type synonym (which of course doesn’t have a constructor; but this is essentially how it reads in the PureScript code, but instead using a sum type with separate constructors instead of the dependent type here, indexed over FeeType). This is much more readable to me (especially in the actual code).

ValidInvoice2 : (ft : FeeType) -> Type
ValidInvoice2 FeeMarkupHidden = ValidArticle FeeMarkupHidden -> Unit            -> ValidInvoice2 FeeMarkupHidden
ValidInvoice2 FeeExplicit     = ValidArticle FeeExplicit     -> Fee FeeExplicit -> ValidInvoice2 FeeExplicit

So why does ValidInvoice4 not type-check? Am I writing it wrong? Or expecting something to work that just can’t work?

imuli imuli · Accepted Answer · 2019-02-08T20:17:34

It appears that Idris isn't noticing that either branch of your case statement results in a ValidInvoice4. It also doesn't evaluate functions in a similar position. You can almost always do something slightly different and get the same result though.

Looking over what you're trying accomplish, I'd recommend making Fee a FeeType-indexed Maybe - which simplifies the whole thing:

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
    HidFee : Fee FeeMarkupHidden
    ExFee : Nat {- or w/e -} -> Fee FeeExplicit

data ValidArticle : (ft : FeeType) -> Type where
    MkVA : ValidArticle ft

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft -> Fee ft -> ValidInvoice ft

Case expression in dependent type not working as expected in Idris

1 Answers