be1569e · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -298,6 +298,9 @@ Extra-source-files:

298 test/reg059/run

299 test/reg059/*.idr

300 test/reg059/expected

301+ test/reg060/run

302+ test/reg060/*.idr

303+ test/reg060/expected

301

304

302 test/basic001/run

305 test/basic001/run

303 test/basic001/*.idr

306 test/basic001/*.idr

src/Idris/Elab/Instance.hs+4−1

@@ -88,6 +88,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

88 -- where block

89 wparams <- mapM (\p -> case p of

90 PApp _ _ args -> getWParams (map getTm args)

91+ a@(PRef fc f) -> getWParams [a]

91 _ -> return []) ps

92 _ -> return []) ps

92 let pnames = map pname (concat (nub wparams))

93 let pnames = map pname (concat (nub wparams))

93 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

94 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

@@ -242,7 +243,9 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

242 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

243 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

243 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

244 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

244

245

246+ mkTyDecl (n, op, t, _)

245− mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

247+ = PTy emptyDocstring [] syn fc op n

248+ (mkUniqueNames [] t)

246

249

247 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

250 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

248 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

251 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

test/reg060/expectednew file

No changes to the content.

test/reg060/reg060.idrnew file+12

@@ -0,0 +1,12 @@

1+

2+class MyFunctor (f : Type -> Type) where

3+ mymap : (m : a -> b) -> f a -> f b

4+

5+data Foo x y = Bar y

6+

7+instance MyFunctor (Foo m) where

8+ mymap m x = ?wibble

9+

10+instance [foo] Functor m => MyFunctor m where

11+ mymap m x = map m x

12+

test/reg060/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg060.idr --check

3+rm -f *.ibc