Idris - Expression doesnt typecheck when imported from module

Question

I have an Idris module that defines a certain type/predicate IsSet and a decidability function isSet over it. It also defines some helper functions to compute that decidability function at type-checking to obtain a proof of IsSet.

Expressions that use that auxiliary function typecheck correctly inside the module, but don't when I define them in another file and I import the original module:

Test1.idr

module Test1

import Data.List

%default total
%access export

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

ifNotSetHereThenNeitherThere : Not (IsSet xs) -> Not (IsSet (x :: xs))
ifNotSetHereThenNeitherThere notXsIsSet (IsSetCons xIsInXs xsIsSet) = notXsIsSet xsIsSet  

ifIsElemThenConsIsNotSet : Elem x xs -> Not (IsSet (x :: xs))      
ifIsElemThenConsIsNotSet xIsInXs (IsSetCons notXIsInXs xsIsSet) = notXIsInXs xIsInXs

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)
isSet [] = Yes IsSetNil
isSet (x :: xs) with (isSet xs)
  isSet (x :: xs) | No notXsIsSet = No $ ifNotSetHereThenNeitherThere notXsIsSet
  isSet (x :: xs) | Yes xsIsSet with (isElem x xs)
    isSet (x :: xs) | Yes xsIsSet | No notXInXs = Yes $ IsSetCons notXInXs xsIsSet
    isSet (x :: xs) | Yes xsIsSet | Yes xInXs = No $ ifIsElemThenConsIsNotSet xInXs

getYes : (d : Dec p) -> case d of { No _ => (); Yes _ => p}
getYes (No _ ) = ()
getYes (Yes prf) = prf

getNo : (d : Dec p) -> case d of { No _ => Not p; Yes _ => ()}
getNo (No cnt) = cnt
getNo (Yes _ ) = ()

setTest1 : IsSet ["x"]
setTest1 = getYes $ isSet ["x"]

Test2.idr

module Test2

import Test1

%default total
%access export

setTest2 : IsSet ["x"]
setTest2 = getYes $ isSet ["x"]

setTest1 typechecks correctly but setTest2 throws the following error:

When checking right hand side of setTest2 with expected type
         IsSet ["x"]

 Type mismatch between
         case block in getYes at Test1.idr:26:30 (IsSet ["x"])
                                                 (isSet ["x"])
                                                 (isSet ["x"]) (Type of getYes (isSet ["x"]))
 and
         IsSet ["x"] (Expected type)

I'm using Idris 0.12

Julian Kniephoff Julian Kniephoff · Accepted Answer · 2016-07-20T13:55:45

When type checking Test2.idr, the type checker does not know the definition (as opposed to just the type) of isSet, so it cannot reduce the type signature of getYes, hence the type mismatch. In order for this to work, you have to public export the function isSet. Due to Idris' visibility rules, you then also have to at least public export the IsSet type, because isSet references its (currently not exported) definition.

This is probably a good idea anyway, though, since without that, not even a simple function like

isNil : IsSet l -> Bool
isNil IsSetNil = True
isNil (IsSetCons f y) = False

in Test2.idr would work, since that module does not know the definition, i.e. the data constructors, of the type.

Idris - Expression doesnt typecheck when imported from module

1 Answers