Allow flagging types as externally defined

e.g. in a C file. This means we don't accidentally treat things as
empty, since previously we just defined these as empty types, but that
broke coverage checking. Fixes #240

libs/base/Data/IORef.idr

@@ -4,7 +4,7 @@ module Data.IORef
 
 -- Implemented externally
 -- e.g., in Scheme, passed around as a box
-data Mut : Type -> Type
+data Mut : Type -> Type where [external]
 
 %extern prim__newIORef : forall a . a -> (1 x : %World) -> IORes (Mut a)
 %extern prim__readIORef : forall a . Mut a -> (1 x : %World) -> IORes a

libs/prelude/PrimIO.idr

@@ -44,14 +44,14 @@ io_bind (MkIO fn)
 -- The parameter is a phantom type, to help differentiate between
 -- different pointer types
 public export
-data Ptr : Type -> Type where
+data Ptr : Type -> Type where [external]
 
 -- A pointer to any type (representing a void* in foreign calls)
 public export
-data AnyPtr : Type where
+data AnyPtr : Type where [external]
 
 public export
-data ThreadID : Type where
+data ThreadID : Type where [external]
 
 public export
 data FArgList : Type where

src/Core/Binary.idr

@@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 19
+ttcVersion = 20
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Context.idr

@@ -36,6 +36,16 @@ export
 defaultPI : PMDefInfo
 defaultPI = MkPMDefInfo NotHole False
 
+public export
+record TypeFlags where
+  constructor MkTypeFlags
+  uniqueAuto : Bool  -- should 'auto' implicits check for uniqueness
+  external : Bool -- defined externally (e.g. in a C or Scheme library)
+
+export
+defaultFlags : TypeFlags
+defaultFlags = MkTypeFlags False False
+
 public export
 data Def : Type where
     None : Def -- Not yet defined
@@ -61,8 +71,7 @@ data Def : Type where
     TCon : (tag : Int) -> (arity : Nat) ->
            (parampos : List Nat) -> -- parameters
            (detpos : List Nat) -> -- determining arguments
-           (uniqueAuto : Bool) -> -- should 'auto' implicits check
-                                  -- for uniqueness
+           (flags : TypeFlags) -> -- should 'auto' implicits check
            (mutwith : List Name) ->
            (datacons : List Name) ->
            (detagabbleBy : Maybe (List Nat)) ->
@@ -1286,7 +1295,7 @@ getSearchData fc defaults target
                      pure (MkSearchData dets (filter (isCons . snd)
                                [(False, opens),
                                 (False, autos),
-                                (not u, tyhs),
+                                (not (uniqueAuto u), tyhs),
                                 (True, chasers)]))
   where
     isDefault : (Name, Bool) -> Bool
@@ -1362,9 +1371,22 @@ setUniqueSearch fc tyn u
     = do defs <- get Ctxt
          Just g <- lookupCtxtExact tyn (gamma defs)
               | _ => throw (UndefinedName fc tyn)
-         let TCon t a ps ds _ cons ms det = definition g
+         let TCon t a ps ds fl cons ms det = definition g
               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
-         updateDef tyn (const (Just (TCon t a ps ds u cons ms det)))
+         let fl' = record { uniqueAuto = u } fl
+         updateDef tyn (const (Just (TCon t a ps ds fl' cons ms det)))
+
+export
+setExternal : {auto c : Ref Ctxt Defs} ->
+              FC -> Name -> Bool -> Core ()
+setExternal fc tyn u
+    = do defs <- get Ctxt
+         Just g <- lookupCtxtExact tyn (gamma defs)
+              | _ => throw (UndefinedName fc tyn)
+         let TCon t a ps ds fl cons ms det = definition g
+              | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
+         let fl' = record { external = u } fl
+         updateDef tyn (const (Just (TCon t a ps ds fl' cons ms det)))
 
 export
 addHintFor : {auto c : Ref Ctxt Defs} ->
@@ -1598,7 +1620,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
                             (TCon tag arity
                                   (paramPos (Resolved tidx) (map type datacons))
                                   (allDet arity)
-                                  False [] (map name datacons) Nothing)
+                                  defaultFlags [] (map name datacons) Nothing)
          (idx, gam') <- addCtxt tyn tydef (gamma defs)
          gam'' <- addDataConstructors 0 datacons gam'
          put Ctxt (record { gamma = gam'' } defs)

src/Core/Coverage.idr

@@ -51,8 +51,10 @@ export
 isEmpty : Defs -> NF vars -> Core Bool
 isEmpty defs (NTCon fc n t a args)
      = case !(lookupDefExact n (gamma defs)) of
-            Just (TCon _ _ _ _ _ _ cons _)
-                 => allM (conflict defs (NTCon fc n t a args)) cons
+            Just (TCon _ _ _ _ flags _ cons _)
+                 => if not (external flags)
+                       then allM (conflict defs (NTCon fc n t a args)) cons
+                       else pure False
             _ => pure False
 isEmpty defs _ = pure False
 

src/Core/TTC.idr

@@ -777,6 +777,16 @@ TTC PMDefInfo where
            r <- fromBuf b
            pure (MkPMDefInfo h r)
 
+export
+TTC TypeFlags where
+  toBuf b l
+      = do toBuf b (uniqueAuto l)
+           toBuf b (external l)
+  fromBuf b
+      = do u <- fromBuf b
+           e <- fromBuf b
+           pure (MkTypeFlags u e)
+
 export
 TTC Def where
   toBuf b None = tag 0

src/Idris/Parser.idr

@@ -894,6 +894,8 @@ dataOpt
   <|> do exactIdent "search"
          ns <- some name
          pure (SearchBy ns)
+  <|> do exactIdent "external"
+         pure External
 
 dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm ->
            EmptyRule PDataDecl

src/TTImp/ProcessData.idr

@@ -27,6 +27,8 @@ processDataOpt fc ndef (SearchBy dets)
     = setDetermining fc ndef dets
 processDataOpt fc ndef UniqueSearch
     = setUniqueSearch fc ndef True
+processDataOpt fc ndef External
+    = setExternal fc ndef True
 
 checkRetType : {auto c : Ref Ctxt Defs} ->
                Env Term vars -> NF vars ->
@@ -253,7 +255,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
 
          -- Add the type constructor as a placeholder
          tidx <- addDef n (newDef fc n Rig1 vars fullty vis
-                          (TCon 0 arity [] [] False [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
          addMutData (Resolved tidx)
          defs <- get Ctxt
          traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)
@@ -306,7 +308,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          -- Add the type constructor as a placeholder while checking
          -- data constructors
          tidx <- addDef n (newDef fc n Rig1 vars fullty vis
-                          (TCon 0 arity [] [] False [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
          case vis of
               Private => pure ()
               _ => do addHash n

src/TTImp/TTImp.idr

@@ -231,12 +231,14 @@ mutual
        SearchBy : List Name -> DataOpt -- determining arguments
        NoHints : DataOpt -- Don't generate search hints for constructors
        UniqueSearch : DataOpt -- auto implicit search must check result is unique
+       External : DataOpt -- implemented externally
 
   export
   Eq DataOpt where
     (==) (SearchBy xs) (SearchBy ys) = xs == ys
     (==) NoHints NoHints = True
     (==) UniqueSearch UniqueSearch = True
+    (==) External External = True
     (==) _ _ = False
 
   public export
@@ -812,6 +814,7 @@ mutual
         = do tag 0; toBuf b ns
     toBuf b NoHints = tag 1
     toBuf b UniqueSearch = tag 2
+    toBuf b External = tag 3
 
     fromBuf b
         = case !getTag of
@@ -819,6 +822,7 @@ mutual
                        pure (SearchBy ns)
                1 => pure NoHints
                2 => pure UniqueSearch
+               3 => pure External
                _ => corrupt "DataOpt"
 
   export

tests/Main.idr

@@ -81,6 +81,7 @@ idrisTests
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
+       "reg015",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",

tests/idris2/reg015/anyfail.idr

@@ -0,0 +1,21 @@
+data SimpleData = PtrAndSize AnyPtr Int
+
+record Complicated where
+  constructor MkComplicated 
+  simple : SimpleData 
+
+record MoreComplicated where
+    constructor MkMoreComplicated
+    something : Complicated
+
+record EvenMoreComplicated where
+    constructor MkEvenMoreComplicated
+    somethingEven : MoreComplicated 
+
+data TooComplicatedToBeTrue : (something : EvenMoreComplicated) -> Type where
+    SomethingVeryComplicatedIs :
+        TooComplicatedToBeTrue
+            (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len))))
+
+showing  :  (something : EvenMoreComplicated) -> (TooComplicatedToBeTrue something) -> Void
+showing _ SomethingVeryComplicatedIs impossible

tests/idris2/reg015/expected

@@ -0,0 +1,2 @@
+1/1: Building anyfail (anyfail.idr)
+anyfail.idr:21:1--22:1:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is not a valid impossible case

tests/idris2/reg015/run

@@ -0,0 +1,3 @@
+$1 anyfail.idr --check
+
+rm -rf build