9297ae4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow 'data' declarations in interfaces

9297ae4Edwin Brady10 years ago

CHANGELOG.md+5

compare with master

unifiedsplit

@@ -29,6 +29,11 @@

29 neutral = 1

30 ```

32+* Interface definitions can now include data declarations (but not data

33+ definitions). Any implementation of the interface must define the method

34+ using a data type. The effect is to cause Idris to treat the method as

35+ a data type (for unification and interface resolution purposes).

36+

32* Experimentally, allow named implementations to be available by default in a

37* Experimentally, allow named implementations to be available by default in a

33 block of declarations with `using` notation. For example:

38 block of declarations with `using` notation. For example:

idris.cabal+3

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

620 test/interfaces004/*.idr

621 test/interfaces004/run

622 test/interfaces004/expected

623+ test/interfaces005/*.idr

624+ test/interfaces005/run

625+ test/interfaces005/expected

623

626

624 test/io001/run

627 test/io001/run

625 test/io001/*.idr

628 test/io001/*.idr

src/IRTS/Compiler.hs+1−1

@@ -439,7 +439,7 @@ irTerm vs env tm@(App _ f a) = do

439 | otherwise = n

440

441 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

442− fst4 (x,_,_,_) = x

442+ fst4 (x,_,_,_,_) = x

443

444irTerm vs env (P _ n _) = return $ LV (Glob n)

445irTerm vs env (V i)

src/Idris/ASTUtils.hs+1−1

@@ -138,7 +138,7 @@ opts_idrisCmdline =

138-------------

139-- This has a terrible name, but I'm not sure of a better one that isn't

140-- confusingly close to tt_ctxt

141−known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))

141+known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))

142known_terms = Field (definitions . tt_ctxt)

143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

144

src/Idris/AbsSyntax.hs+6

@@ -218,6 +218,12 @@ setTotality n a

218 let ctxt = setTotal n a (tt_ctxt i)

219 putIState $ i { tt_ctxt = ctxt }

220

221+setInjectivity :: Name -> Injectivity -> Idris ()

222+setInjectivity n a

223+ = do i <- getIState

224+ let ctxt = setInjective n a (tt_ctxt i)

225+ putIState $ i { tt_ctxt = ctxt }

226+

221getTotality :: Name -> Idris Totality

227getTotality :: Name -> Idris Totality

222getTotality n

228getTotality n

223 = do i <- getIState

229 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+3−1

@@ -333,6 +333,7 @@ data IBCWrite = IBCFix FixDecl

333 | IBCAccess Name Accessibility

334 | IBCMetaInformation Name MetaInformation

335 | IBCTotal Name Totality

336+ | IBCInjective Name Injectivity

336 | IBCFlags Name [FnOpt]

337 | IBCFlags Name [FnOpt]

337 | IBCFnInfo Name FnInfo

338 | IBCFnInfo Name FnInfo

338 | IBCTrans Name (Term, Term)

339 | IBCTrans Name (Term, Term)

@@ -775,6 +776,7 @@ data Directive = DLib Codegen String

775 | DInclude Codegen String

776 | DInclude Codegen String

776 | DHide Name

777 | DHide Name

777 | DFreeze Name

778 | DFreeze Name

779+ | DInjective Name

778 | DAccess Accessibility

780 | DAccess Accessibility

779 | DDefault DefaultTotality

781 | DDefault DefaultTotality

780 | DLogging Integer

782 | DLogging Integer

@@ -1377,7 +1379,7 @@ highestFC (PAppImpl t _) = highestFC t

1377-- Type class data

1379-- Type class data

1378

1380

1379data ClassInfo = CI { instanceCtorName :: Name,

1381data ClassInfo = CI { instanceCtorName :: Name,

1380− class_methods :: [(Name, (FnOpts, PTerm))],

1382+ class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method

1381 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

1383 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

1382 class_default_superclasses :: [PDecl],

1384 class_default_superclasses :: [PDecl],

1383 class_params :: [Name],

1385 class_params :: [Name],

src/Idris/CaseSplit.hs+2−2

@@ -410,10 +410,10 @@ getClause l fn un fp

410 sUN "z"]) used

411

412 -- write method declarations, indent with 4 spaces

413− mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

413+ mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

414 mkClassBodies i ns

415 = showSep "\n"

416− (zipWith (\(n, (_, ty)) m -> " " ++

416+ (zipWith (\(n, (_, _, ty)) m -> " " ++

417 def (show (nsroot n)) ++ " "

418 ++ mkApp i ty []

419 ++ "= ?"

src/Idris/Core/Evaluate.hs+45−32

@@ -6,14 +6,15 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

6 normaliseAll, normaliseBlocking, toValue, quoteTerm,

7 rt_simplify, simplify, specialise, hnf, convEq, convEq',

8 Def(..), CaseInfo(..), CaseDefs(..),

9− Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

9+ Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),

10 Context, initContext, ctxtAlist, next_tvar,

11− addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

11+ addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

12 addDatatype, addCasedef, simplifyCasedef, addOperator,

13 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

14 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

15 mapDefCtxt,

16+ lookupTotal, lookupTotalExact, lookupInjectiveExact,

16− lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

17+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

17 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

18 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

18 isUniverse) where

19 isUniverse) where

@@ -759,6 +760,8 @@ instance Show Accessibility where

759 show Private = "private"

760 show Private = "private"

760 show Hidden = "hidden"

761 show Hidden = "hidden"

761

762

763+type Injectivity = Bool

764+

762-- | The result of totality checking

765-- | The result of totality checking

763data Totality = Total [Int] -- ^ well-founded arguments

766data Totality = Total [Int] -- ^ well-founded arguments

764 | Productive -- ^ productive

767 | Productive -- ^ productive

@@ -816,7 +819,7 @@ data MetaInformation =

816-- universe constraints and existing definitions.

819-- universe constraints and existing definitions.

817data Context = MkContext {

820data Context = MkContext {

818 next_tvar :: Int,

821 next_tvar :: Int,

819− definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)

822+ definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)

820 } deriving Show

823 } deriving Show

821

824

822

825

@@ -826,47 +829,53 @@ initContext = MkContext 0 emptyContext

826

829

827mapDefCtxt :: (Def -> Def) -> Context -> Context

830mapDefCtxt :: (Def -> Def) -> Context -> Context

828mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)

831mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)

829− where f' (!d, a, t, m) = f' (f d, a, t, m)

832+ where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)

830

833

831-- | Get the definitions from a context

834-- | Get the definitions from a context

832ctxtAlist :: Context -> [(Name, Def)]

835ctxtAlist :: Context -> [(Name, Def)]

833−ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

836+ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

834

837

835veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

838veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

836

839

837addToCtxt :: Name -> Term -> Type -> Context -> Context

840addToCtxt :: Name -> Term -> Type -> Context -> Context

838addToCtxt n tm ty uctxt

841addToCtxt n tm ty uctxt

839 = let ctxt = definitions uctxt

842 = let ctxt = definitions uctxt

840− !ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in

843+ !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in

841 uctxt { definitions = ctxt' }

844 uctxt { definitions = ctxt' }

842

845

843setAccess :: Name -> Accessibility -> Context -> Context

846setAccess :: Name -> Accessibility -> Context -> Context

844setAccess n a uctxt

847setAccess n a uctxt

845 = let ctxt = definitions uctxt

848 = let ctxt = definitions uctxt

846− !ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in

849+ !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in

850+ uctxt { definitions = ctxt' }

851+

852+setInjective :: Name -> Injectivity -> Context -> Context

853+setInjective n i uctxt

854+ = let ctxt = definitions uctxt

855+ !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in

847 uctxt { definitions = ctxt' }

856 uctxt { definitions = ctxt' }

848

857

849setTotal :: Name -> Totality -> Context -> Context

858setTotal :: Name -> Totality -> Context -> Context

850setTotal n t uctxt

859setTotal n t uctxt

851 = let ctxt = definitions uctxt

860 = let ctxt = definitions uctxt

852− !ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in

861+ !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in

853 uctxt { definitions = ctxt' }

862 uctxt { definitions = ctxt' }

854

863

855setMetaInformation :: Name -> MetaInformation -> Context -> Context

864setMetaInformation :: Name -> MetaInformation -> Context -> Context

856setMetaInformation n m uctxt

865setMetaInformation n m uctxt

857 = let ctxt = definitions uctxt

866 = let ctxt = definitions uctxt

858− !ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in

867+ !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in

859 uctxt { definitions = ctxt' }

868 uctxt { definitions = ctxt' }

860

869

861addCtxtDef :: Name -> Def -> Context -> Context

870addCtxtDef :: Name -> Def -> Context -> Context

862addCtxtDef n d c = let ctxt = definitions c

871addCtxtDef n d c = let ctxt = definitions c

863− !ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in

872+ !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in

864 c { definitions = ctxt' }

873 c { definitions = ctxt' }

865

874

866addTyDecl :: Name -> NameType -> Type -> Context -> Context

875addTyDecl :: Name -> NameType -> Type -> Context -> Context

867addTyDecl n nt ty uctxt

876addTyDecl n nt ty uctxt

868 = let ctxt = definitions uctxt

877 = let ctxt = definitions uctxt

869− !ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in

878+ !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in

870 uctxt { definitions = ctxt' }

879 uctxt { definitions = ctxt' }

871

880

872addDatatype :: Datatype Name -> Context -> Context

881addDatatype :: Datatype Name -> Context -> Context

@@ -874,14 +883,14 @@ addDatatype (Data n tag ty unique cons) uctxt

874 = let ctxt = definitions uctxt

883 = let ctxt = definitions uctxt

875 ty' = normalise uctxt [] ty

884 ty' = normalise uctxt [] ty

876 !ctxt' = addCons 0 cons (addDef n

885 !ctxt' = addCons 0 cons (addDef n

877− (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in

886+ (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in

878 uctxt { definitions = ctxt' }

887 uctxt { definitions = ctxt' }

879 where

888 where

880 addCons tag [] ctxt = ctxt

889 addCons tag [] ctxt = ctxt

881 addCons tag ((n, ty) : cons) ctxt

890 addCons tag ((n, ty) : cons) ctxt

882 = let ty' = normalise uctxt [] ty in

891 = let ty' = normalise uctxt [] ty in

883 addCons (tag+1) cons (addDef n

892 addCons (tag+1) cons (addDef n

884− (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

893+ (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)

885

894

886-- FIXME: Too many arguments! Refactor all these Bools.

895-- FIXME: Too many arguments! Refactor all these Bools.

887--

896--

@@ -923,7 +932,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

923 (args_rt, sc_rt)

932 (args_rt, sc_rt)

924 op = (CaseOp (ci { case_inlinable = inlc })

933 op = (CaseOp (ci { case_inlinable = inlc })

925 ty argtys ps_in ps_tot cdef,

934 ty argtys ps_in ps_tot cdef,

926− access, Unchecked, EmptyMI)

935+ False, access, Unchecked, EmptyMI)

927 in return $ addDef n op ctxt

936 in return $ addDef n op ctxt

928-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

937-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

929 return uctxt { definitions = ctxt' }

938 return uctxt { definitions = ctxt' }

@@ -933,15 +942,15 @@ simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

933simplifyCasedef n ei uctxt

942simplifyCasedef n ei uctxt

934 = do let ctxt = definitions uctxt

943 = do let ctxt = definitions uctxt

935 ctxt' <- case lookupCtxt n ctxt of

944 ctxt' <- case lookupCtxt n ctxt of

936− [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

945+ [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->

937 return ctxt -- nothing to simplify (or already done...)

946 return ctxt -- nothing to simplify (or already done...)

938− [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

947+ [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->

939 do let ps_in' = map simpl ps_in

948 do let ps_in' = map simpl ps_in

940 pdef = map debind ps_in'

949 pdef = map debind ps_in'

941 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

950 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

942 return $ addDef n (CaseOp ci

951 return $ addDef n (CaseOp ci

943 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

952 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

944− acc, tot, metainf) ctxt

953+ inj, acc, tot, metainf) ctxt

945

954

946 _ -> return ctxt

955 _ -> return ctxt

947 return uctxt { definitions = ctxt' }

956 return uctxt { definitions = ctxt' }

@@ -961,10 +970,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

961 Context -> Context

970 Context -> Context

962addOperator n ty a op uctxt

971addOperator n ty a op uctxt

963 = let ctxt = definitions uctxt

972 = let ctxt = definitions uctxt

964− ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in

973+ ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in

965 uctxt { definitions = ctxt' }

974 uctxt { definitions = ctxt' }

966

975

967−tfst (a, _, _, _) = a

976+tfst (a, _, _, _, _) = a

968

977

969lookupNames :: Name -> Context -> [Name]

978lookupNames :: Name -> Context -> [Name]

970lookupNames n ctxt

979lookupNames n ctxt

@@ -1041,10 +1050,10 @@ lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]

1041lookupP_all all exact n ctxt

1050lookupP_all all exact n ctxt

1042 = do (n', def) <- names

1051 = do (n', def) <- names

1043 p <- case def of

1052 p <- case def of

1044− (Function ty tm, a, _, _) -> return (P Ref n' ty, a)

1053+ (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)

1045− (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)

1054+ (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)

1046− (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n' ty, a)

1055+ (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)

1047− (Operator ty _ _, a, _, _) -> return (P Ref n' ty, a)

1056+ (Operator ty _ _, inj, a, _, _) -> return (P Ref n' ty, a)

1048 case snd p of

1057 case snd p of

1049 Hidden -> if all then return (fst p) else []

1058 Hidden -> if all then return (fst p) else []

1050 Private -> if all then return (fst p) else []

1059 Private -> if all then return (fst p) else []

@@ -1071,24 +1080,28 @@ lookupDefAcc :: Name -> Bool -> Context ->

1071lookupDefAcc n mkpublic ctxt

1080lookupDefAcc n mkpublic ctxt

1072 = map mkp $ lookupCtxt n (definitions ctxt)

1081 = map mkp $ lookupCtxt n (definitions ctxt)

1073 -- io_bind a special case for REPL prettiness

1082 -- io_bind a special case for REPL prettiness

1074− where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1083+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1075− then (d, Public) else (d, a)

1084+ then (d, Public) else (d, a)

1076

1085

1077lookupDefAccExact :: Name -> Bool -> Context ->

1086lookupDefAccExact :: Name -> Bool -> Context ->

1078 Maybe (Def, Accessibility)

1087 Maybe (Def, Accessibility)

1079lookupDefAccExact n mkpublic ctxt

1088lookupDefAccExact n mkpublic ctxt

1080 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

1089 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

1081 -- io_bind a special case for REPL prettiness

1090 -- io_bind a special case for REPL prettiness

1082− where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1091+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1083− then (d, Public) else (d, a)

1092+ then (d, Public) else (d, a)

1084

1093

1085lookupTotal :: Name -> Context -> [Totality]

1094lookupTotal :: Name -> Context -> [Totality]

1086lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

1095lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

1087− where mkt (d, a, t, m) = t

1096+ where mkt (d, inj, a, t, m) = t

1088

1097

1089lookupTotalExact :: Name -> Context -> Maybe Totality

1098lookupTotalExact :: Name -> Context -> Maybe Totality

1090lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1099lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1091− where mkt (d, a, t, m) = t

1100+ where mkt (d, inj, a, t, m) = t

1101+

1102+lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

1103+lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1104+ where mkt (d, inj, a, t, m) = inj

1092

1105

1093-- Check if a name is reducible in the type checker. Partial definitions

1106-- Check if a name is reducible in the type checker. Partial definitions

1094-- are not reducible (so treated as a constant)

1107-- are not reducible (so treated as a constant)

@@ -1100,10 +1113,10 @@ tcReducible n ctxt = case lookupTotalExact n ctxt of

1100

1113

1101lookupMetaInformation :: Name -> Context -> [MetaInformation]

1114lookupMetaInformation :: Name -> Context -> [MetaInformation]

1102lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

1115lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

1103− where mkm (d, a, t, m) = m

1116+ where mkm (d, inj, a, t, m) = m

1104

1117

1105lookupNameTotal :: Name -> Context -> [(Name, Totality)]

1118lookupNameTotal :: Name -> Context -> [(Name, Totality)]

1106−lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

1119+lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

1107

1120

1108

1121

1109lookupVal :: Name -> Context -> [Value]

1122lookupVal :: Name -> Context -> [Value]

src/Idris/Core/Unify.hs+3−1

@@ -292,6 +292,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

292

293 injective (P (DCon _ _ _) _ _) = True

294 injective (P (TCon _ _) _ _) = True

295+ injective (P Ref n _)

296+ | Just i <- lookupInjectiveExact n ctxt = i

295 injective (App _ f a) = injective f -- && injective a

297 injective (App _ f a) = injective f -- && injective a

296 injective _ = False

298 injective _ = False

297

299

@@ -573,7 +575,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

573

575

574 rigid (P (DCon _ _ _) _ _) = True

576 rigid (P (DCon _ _ _) _ _) = True

575 rigid (P (TCon _ _) _ _) = True

577 rigid (P (TCon _ _) _ _) = True

576− rigid t@(P Ref _ _) = inenv t || globmetavar t

578+ rigid t@(P Ref _ _) = inenv t || globmetavar t

577 rigid (Constant _) = True

579 rigid (Constant _) = True

578 rigid (App _ f a) = rigid f && rigid a

580 rigid (App _ f a) = rigid f && rigid a

579 rigid t = not (metavar t) || globmetavar t

581 rigid t = not (metavar t) || globmetavar t

src/Idris/Core/WHNF.hs+1

@@ -75,6 +75,7 @@ do_whnf ctxt env tm = eval env [] tm

75 = let wp = case nt of

76 DCon t a u -> WDCon t a u n (ty, env)

77 TCon t a -> WTCon t a n (ty, env)

78+ Ref -> WPRef n (ty, env)

78 _ -> WPRef n (ty, env)

79 _ -> WPRef n (ty, env)

79 in

80 in

80 case lookupDefExact n ctxt of

81 case lookupDefExact n ctxt of

src/Idris/DeepSeq.hs+1

@@ -284,6 +284,7 @@ instance NFData IBCWrite where

284 rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()

285 rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()

286 rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()

287+ rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` ()

287 rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()

288 rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()

288 rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()

289 rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()

289 rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()

290 rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()

src/Idris/Directives.hs+5

@@ -42,6 +42,11 @@ directiveAction (DFreeze n') = do

42 mapM_ (\n -> do

43 setAccessibility n Frozen

44 addIBC (IBCAccess n Frozen)) ns

45+directiveAction (DInjective n') = do

46+ ns <- allNamespaces n'

47+ mapM_ (\n -> do

48+ setInjectivity n True

49+ addIBC (IBCInjective n True)) ns

46directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })

51directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })

src/Idris/Elab/Class.hs+24−6

@@ -119,6 +119,11 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

119 -- Elaborate the the top level methods

120 mapM_ (rec_elabDecl info EAll info) (concat fns)

121

122+ -- Flag all the top level data declarations as injective

123+ mapM_ (\n -> do setInjectivity n True

124+ addIBC (IBCInjective n True))

125+ (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))

126+

122 -- add the default definitions

127 -- add the default definitions

123 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

128 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

124 addIBC (IBCClass tn)

129 addIBC (IBCClass tn)

@@ -130,7 +135,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

130 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

135 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

131

136

132 where

137 where

133− nodoc (n, (_, _, o, t)) = (n, (o, t))

138+ nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))

134

139

135 pibind [] x = x

140 pibind [] x = x

136 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

141 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

@@ -171,14 +176,26 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

171 conbind [] x = x

176 conbind [] x = x

172

177

173 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

178 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

179+ getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n

180+

174 tdecl allmeths (PTy doc _ syn _ o n nfc t)

181 tdecl allmeths (PTy doc _ syn _ o n nfc t)

175 = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

182 = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

176 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

183 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

177 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

184 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

185+ (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

186+ (\ l s p -> Imp l s p Nothing True) t'))),

187+ (n, (nfc, syn, o, t) ) )

188+ tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

189+ = do let o = []

190+ t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

191+ logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

192+ return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

178− (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

193+ (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

179 (\ l s p -> Imp l s p Nothing True) t'))),

194 (\ l s p -> Imp l s p Nothing True) t'))),

180 (n, (nfc, syn, o, t) ) )

195 (n, (nfc, syn, o, t) ) )

196+ tdecl allmeths (PData doc _ syn _ _ _)

197+ = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")

181− tdecl _ _ = ifail "Not allowed in a class declaration"

198+ tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")

182

199

183 -- Create default definitions

200 -- Create default definitions

184 defdecl mtys c d@(PClauses fc opts n cs) =

201 defdecl mtys c d@(PClauses fc opts n cs) =

@@ -190,13 +207,14 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

190 PClauses fc (o ++ opts) n cs]

207 PClauses fc (o ++ opts) n cs]

191 logElab 1 (show ds)

208 logElab 1 (show ds)

192 return (n, ((defaultdec n, ds!!1), ds))

209 return (n, ((defaultdec n, ds!!1), ds))

193− _ -> ifail $ show n ++ " is not a method"

210+ _ -> ierror $ At fc (Msg (show n ++ " is not a method"))

194 defdecl _ _ _ = ifail "Can't happen (defdecl)"

211 defdecl _ _ _ = ifail "Can't happen (defdecl)"

195

212

196 defaultdec (UN n) = sUN ("default#" ++ str n)

213 defaultdec (UN n) = sUN ("default#" ++ str n)

197 defaultdec (NS n ns) = NS (defaultdec n) ns

214 defaultdec (NS n ns) = NS (defaultdec n) ns

198

215

199 tydecl (PTy{}) = True

216 tydecl (PTy{}) = True

217+ tydecl (PData _ _ _ _ _ _) = True

200 tydecl _ = False

218 tydecl _ = False

201 instdecl (PInstance{}) = True

219 instdecl (PInstance{}) = True

202 instdecl _ = False

220 instdecl _ = False

@@ -233,10 +251,10 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

233 tfun :: Name -- ^ The name of the class

251 tfun :: Name -- ^ The name of the class

234 -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

252 -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

235 -> SyntaxInfo -> [Name] -- ^ All the method names

253 -> SyntaxInfo -> [Name] -- ^ All the method names

236− -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))

254+ -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))

237 -- ^ The present declaration

255 -- ^ The present declaration

238 -> Idris [PDecl]

256 -> Idris [PDecl]

239− tfun cn c syn all (m, (mfc, doc, o, ty))

257+ tfun cn c syn all (m, (isdata, mfc, doc, o, ty))

240 = do let ty' = expandMethNS syn (insertConstraint c all ty)

258 = do let ty' = expandMethNS syn (insertConstraint c all ty)

241 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

259 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

242 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

260 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

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

@@ -123,7 +123,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

123 logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

124

125 let all_meths = map (nsroot . fst) (class_methods ci)

126− let mtys = map (\ (n, (op, t)) ->

126+ let mtys = map (\ (n, (inj, op, t)) ->

127 let t_in = substMatchesShadow ips pnames t

128 mnamemap =

129 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

@@ -139,6 +139,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

139 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

140 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

141 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

142+

142 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

143 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

143 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

144 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

144 let wbTys = map mkTyDecl mtys

145 let wbTys = map mkTyDecl mtys

@@ -187,6 +188,8 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

187 let wbVals' = map (addParams prop_params) wbVals

188 let wbVals' = map (addParams prop_params) wbVals

188

189

189 mapM_ (rec_elabDecl info EAll info) wbVals'

190 mapM_ (rec_elabDecl info EAll info) wbVals'

191+

192+ mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')

190

193

191 pop_estack

194 pop_estack

192

195

@@ -436,6 +439,37 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

436

439

437addParams ps d = d

440addParams ps d = d

438

441

442+-- Check a given method definition is injective, if the class info

443+-- says it needs to be.

444+-- Takes originally written decl and the one with name decoration, so

445+-- we know which name to look up.

446+checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->

447+ (PDecl, PDecl) -> Idris ()

448+checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

449+ | Just (True, _, _) <- clookup n ns

450+ = do ist <- getIState

451+ case lookupDefExact elabn (tt_ctxt ist) of

452+ Just (CaseOp _ _ _ _ _ cdefs) ->

453+ checkInjectiveCase ist (snd (cases_compiletime cdefs))

454+ where

455+ checkInjectiveCase ist (STerm tm)

456+ = checkInjectiveApp ist (fst (unApply tm))

457+ checkInjectiveCase _ _ = notifail

458+

459+ checkInjectiveApp ist (P (TCon _ _) n _) = return ()

460+ checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()

461+ checkInjectiveApp ist (P Ref n _)

462+ | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()

463+ checkInjectiveApp ist (P Ref n _) = notifail

464+ checkInjectiveApp _ _ = notifail

465+

466+ notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))

467+

468+ clookup n [] = Nothing

469+ clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d

470+ | otherwise = Nothing

471+checkInjectiveDef fc ns _ = return()

472+

439checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

473checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

440checkInjectiveArgs fc n ds Nothing = return ()

474checkInjectiveArgs fc n ds Nothing = return ()

441checkInjectiveArgs fc n ds (Just ty)

475checkInjectiveArgs fc n ds (Just ty)

src/Idris/IBC.hs+11−2

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 140

43+ibcVersion = 141

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

@@ -95,6 +95,7 @@ data IBCFile = IBCFile { ver :: Word16,

95 ibc_deprecated :: ![(Name, String)],

96 ibc_defs :: ![(Name, Def)],

97 ibc_total :: ![(Name, Totality)],

98+ ibc_injective :: ![(Name, Injectivity)],

98 ibc_access :: ![(Name, Accessibility)],

99 ibc_access :: ![(Name, Accessibility)],

99 ibc_fragile :: ![(Name, String)]

100 ibc_fragile :: ![(Name, String)]

100 }

101 }

@@ -104,7 +105,7 @@ deriving instance Binary IBCFile

104!-}

105!-}

105

106

106initIBC :: IBCFile

107initIBC :: IBCFile

107−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] []

108+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] []

108

109

109hasValidIBCVersion :: FilePath -> Idris Bool

110hasValidIBCVersion :: FilePath -> Idris Bool

110hasValidIBCVersion fp = do

111hasValidIBCVersion fp = do

@@ -197,6 +198,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

197 makeEntry "ibc_deprecated" (ibc_deprecated i),

198 makeEntry "ibc_deprecated" (ibc_deprecated i),

198 makeEntry "ibc_defs" (ibc_defs i),

199 makeEntry "ibc_defs" (ibc_defs i),

199 makeEntry "ibc_total" (ibc_total i),

200 makeEntry "ibc_total" (ibc_total i),

201+ makeEntry "ibc_injective" (ibc_injective i),

200 makeEntry "ibc_access" (ibc_access i),

202 makeEntry "ibc_access" (ibc_access i),

201 makeEntry "ibc_fragile" (ibc_fragile i)]

203 makeEntry "ibc_fragile" (ibc_fragile i)]

202

204

@@ -300,6 +302,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

300ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

302ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

301ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

303ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

302ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

304ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

305+ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }

303ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

306ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

304ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

307ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

305ibc i (IBCLineApp fp l t) f

308ibc i (IBCLineApp fp l t) f

@@ -394,6 +397,7 @@ process reexp phase archive fn = do

394 processDeprecate archive

397 processDeprecate archive

395 processDefs archive

398 processDefs archive

396 processTotal archive

399 processTotal archive

400+ processInjective archive

397 processAccess reexp phase archive

401 processAccess reexp phase archive

398 processFragile archive

402 processFragile archive

399

403

@@ -718,6 +722,11 @@ processTotal ar = do

718 ds <- getEntry [] "ibc_total" ar

722 ds <- getEntry [] "ibc_total" ar

719 mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

723 mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

720

724

725+processInjective :: Archive -> Idris ()

726+processInjective ar = do

727+ ds <- getEntry [] "ibc_injective" ar

728+ mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setInjective n a (tt_ctxt i) })) ds

729+

721processTotalityCheckError :: Archive -> Idris ()

730processTotalityCheckError :: Archive -> Idris ()

722processTotalityCheckError ar = do

731processTotalityCheckError ar = do

723 es <- getEntry [] "ibc_totcheckfail" ar

732 es <- getEntry [] "ibc_totcheckfail" ar

src/Idris/Parser.hs+8−1

@@ -877,7 +877,10 @@ classBlock syn = do reservedHL "where"

877 ist <- get

878 let cd' = annotate syn ist cd

879

880− ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)

880+ ds <- many (notEndBlock >> try (instance_ True syn)

881+ <|> do x <- data_ syn

882+ return [x]

883+ <|> fnDecl syn)

881 closeBlock

884 closeBlock

882 return (cn, cd', concat ds)

885 return (cn, cd', concat ds)

883 <?> "class block"

886 <?> "class block"

@@ -1377,6 +1380,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

1377 return [PDirective (DHide n)]

1380 return [PDirective (DHide n)]

1378 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

1381 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

1379 return [PDirective (DFreeze n)]

1382 return [PDirective (DFreeze n)]

1383+ -- injectivity assertins are intended for debugging purposes

1384+ -- only, and won't be documented/could be removed at any point

1385+ <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

1386+ return [PDirective (DInjective n)]

1380 <|> do try (lchar '%' *> reserved "access")

1387 <|> do try (lchar '%' *> reserved "access")

1381 acc <- accessibility

1388 acc <- accessibility

1382 ist <- get

1389 ist <- get

src/Idris/Parser/Data.hs+11−7

@@ -204,18 +204,21 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

204 fc <- getFC

205 (tyn_in, nfc) <- fnName

206 (do try (lchar ':')

207− popIndent

208 ty <- typeExpr (allowImp syn)

207 ty <- typeExpr (allowImp syn)

209 let tyn = expandNS syn tyn_in

208 let tyn = expandNS syn tyn_in

210− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

209+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

211 reservedHL "where"

210 reservedHL "where"

212 cons <- indentedBlock (constructor syn)

211 cons <- indentedBlock (constructor syn)

213 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

212 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

214− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do

213+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))

214+ terminator

215+ return d) <|> (do

216+ args <- many (do notEndApp

215− args <- many (fst <$> name)

217+ x <- fst <$> name

218+ return x)

216 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

219 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

217 let tyn = expandNS syn tyn_in

220 let tyn = expandNS syn tyn_in

218− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

221+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

219 try (lchar '=') <|> do reservedHL "where"

222 try (lchar '=') <|> do reservedHL "where"

220 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

223 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

221 let n = show tyn_in ++ " "

224 let n = show tyn_in ++ " "

@@ -228,13 +231,14 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

228 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

231 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

229 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

232 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

230 cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

233 cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

231− terminator

232 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

234 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

233 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

235 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

234 do let cty = bindArgs cargs conty

236 do let cty = bindArgs cargs conty

235 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

237 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

236 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')

238 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')

237− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons')))

239+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))

240+ terminator

241+ return d)

238 <?> "data type declaration"

242 <?> "data type declaration"

239 where

243 where

240 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

244 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

src/Idris/TypeSearch.hs+2−2

@@ -92,8 +92,8 @@ searchPred istate ty1 = matcher where

92 matcher = matchTypesBulk istate maxScore ty1

95−typeFromDef :: (Def, b, c, d) -> Maybe Type

95+typeFromDef :: (Def, i, b, c, d) -> Maybe Type

96−typeFromDef (def, _, _, _) = get def where

96+typeFromDef (def, _, _, _, _) = get def where

97 get :: Def -> Maybe Type

98 get (Function ty _) = Just ty

99 get (TyDecl _ ty) = Just ty