Search code examples
printftypeerrortypecheckingtype-mismatchidris

Cannot match two identical types

I don't really know how to properly address this since I'm new to Idris, so I'll tell my story.

I was implementing a type-safe sprintf function, with the following type signature:

sprintf : (s: String) -> typeListToFunc String (corresArgs (toPrintf (unpack s)))

Where that big pile of stuff basically looks for printf specifiers within the string and generate required arguments in term of a function. For example, "%c%f%d" would give Char -> Double -> Int -> String, and "" would simply give String.

Although this implementation works fine, it is unable to pass the tests by failing the type check. Here's a quick peek:

import Specdris.Spec
import Sprintf

specSuite : IO ()
specSuite = spec $ do
  describe "Fixed tests" $ do
    it "Should accept no arg when no fmt" $ do
      sprintf "" `shouldBe` ""  -- this is line 13

In particular, Idris could not find a match between String and typeListToFunc String (corresArgs (toPrintf (unpack ""))):

Type checking ./Sprintf.idr
Type checking ./SprintfSpec.idr
SprintfSpec.idr:10:13-24:108:
   |
10 | specSuite = spec $ do
   |             ~~~~~~~~~ ...
When checking right hand side of specSuite with expected type
        IO ()

When checking an application of function Specdris.Data.SpecResult.SpecResultDo.>>=:
        Can't find implementation for Show (typeListToFunc String (corresArgs (toPrintf (unpack ""))))

        Possible cause:
                SprintfSpec.idr:13:18-27:When checking argument expected to function Specdris.Expectations.shouldBe:
                        Type mismatch between
                                String (Type of "")
                        and
                                typeListToFunc String (corresArgs (toPrintf (unpack ""))) (Expected type)

                        Specifically:
                                Type mismatch between
                                        String
                                and
                                        typeListToFunc String (corresArgs (toPrintf []))

As aforementioned, they are really the same type:

$ idris Sprintf.idr
*Sprintf> typeListToFunc String (corresArgs (toPrintf (unpack "")))
String : Type

Yeah, I'm really confused why couldn't Idris just get around this. FWIW I have put my source file and test spec on GitHub if anyone would like to look in details.

Solution

  • Turns out people came before have already realised this issue. Quote from Voile in this thread:

    Every data type and type level function must be public exported in order for the test module to see them (and the same goes to the test module to main), so %access public export should be the default for almost all cases. This throws people (read: me when solving a Idris kata) off because e.g Try It Online does not need it (code are in the same module as Main.main).

    Add %access public export solves the issue.