Compiler crash (scope error)

[treeowl]

The error message is rather short:

idris: Scope error in !!V 5!!

The code producing it is also reasonably short:

module WF

Pred : Type -> Type
Pred a = a -> Type

Subset : Pred a -> Pred a -> Type
Subset {a} P1 P2 = {x : a} -> P1 x -> P2 x

subsetBuild : (a : Type) -> (Q : Pred a) -> (Rec : Pred a -> Pred a) ->
              ((P : Pred a) -> Rec P `Subset` P -> Q `Subset` Rec P) ->
              ((P : Pred a) -> Rec P `Subset` P -> Q `Subset` P)
subsetBuild a Q Rec builder P f x q = f x (builder P f x q)

[treeowl]

In case this helps, replacing the right-hand side of subsetBuild with a metavariable still gives the same crash.

[treeowl]

Here's another one. With these definitions:

Rel : (a : Type) -> Type
Rel a = a -> a -> Type

||| Take the transitive closure of a relation
data TC : Rel t -> Rel t where
  TCIncl : r x y -> TC r x y
  TCTrans : TC r x y -> TC r y z -> TC r x z

class Transitive (rel : Rel a) where
  trans : x `rel` y -> y `rel` z -> x `rel` z

TransitiveR : Rel a -> Type
TransitiveR {a} rel = {x,y,z:a} -> x `rel` y -> y `rel` z -> x `rel` z

instance Transitive (TC rel) where
  trans xRy yRz = TCTrans xRy yRz

I'd like to define

TcTransitive : TransitiveR (TC r)
TcTransitive xRy xRz = trans xRy xRz

but the compiler spits out Scope error in !!V 1!! and crashes. Instead, I have to define

TcTransitive : TC r x y -> TC r y z -> TC r x z
TcTransitive xRy xRz = trans xRy xRz

[ahmadsalim]

I am now getting a sensible error:

Type checking ./test.idr
test.idr:12:13:When checking left hand side of subsetBuild:
subsetBuild a Q Rec builder P f x x does not have a function type (P x)
Holes: WF.subsetBuild