Pattern matching on the result of type computing functions in idris

Question

Consider the following fragment:

import Data.List

%default total

x : Elem 1 [1, 2]
x = Here

type : Type
type = Elem 1 [1, 2]

y : type
y = Here

This gives the error:

When checking right hand side of y: Type mismatch between Elem x (x :: xs) (Type of Here) and iType (Expected type)

The type of y, when queried, is:

type : Type
-----------
y : type

Is it possible to force type to be evaluated during or before the type ascription of y, so that the type of y is Elem 1 [1, 2]?

My use case is that I want to be able to define generic predicates that return the right proposition terms for proofs, for example:

subset : List a -> List a -> Type
subset xs ys = (e : a) -> Elem e xs -> Elem e ys

thm_filter_subset : subset (filter p xs) xs

Edwin Brady Edwin Brady · Accepted Answer · 2015-10-15T12:18:45

Names in type declarations which begin with a lower case letter are implicitly bound, so it's treating 'type' as a type parameter. You can either give 'type' a new name which begins with a capital (by convention this is what most people do in Idris) or you can explicitly qualify the name with the module it's in (Main, here).

Idris used to try guessing whether names such as 'type' were intended as an implicit or intended to refer to the global, as here. There's all kinds of voodoo involved in getting this right though, so it often failed, and so it now implements this much simpler rule. It's slightly annoying in cases such as this, but the alternative behaviour was more often annoying (and harder to explain).

Pattern matching on the result of type computing functions in idris

1 Answers