183f533 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Deal with ambiguity in impossible clauses

183f533Edwin Brady10 years ago

src/Idris/Coverage.hs+56−22

compare with master

unifiedsplit

@@ -14,6 +14,7 @@ import Idris.Core.CaseTree

14import Idris.Core.Evaluate

15import Idris.Core.TT

16import Idris.Delaborate

17+import Idris.Elab.Utils

17import Idris.Error

18import Idris.Error

18import Idris.Output (iWarn, iputStrLn)

19import Idris.Output (iWarn, iputStrLn)

@@ -28,33 +29,64 @@ import Debug.Trace

28--

29--

29-- We need this to eliminate the pattern clauses which have been

30-- We need this to eliminate the pattern clauses which have been

30-- provided explicitly from new clause generation.

31-- provided explicitly from new clause generation.

32+--

33+-- This takes a type directed approach to disambiguating names. If we

34+-- can't immediately disambiguate by looking at the expected type, it's an

35+-- error (we can't do this the usual way of trying it to see what type checks

36+-- since the whole point of an impossible case is that it won't type check!)

31mkPatTm :: PTerm -> Idris Term

37mkPatTm :: PTerm -> Idris Term

32mkPatTm t = do i <- getIState

38mkPatTm t = do i <- getIState

33 let timp = addImpl' True [] [] [] i t

39 let timp = addImpl' True [] [] [] i t

34− evalStateT (toTT (mapPT deNS timp)) 0

40+ evalStateT (toTT Nothing timp) 0

35 where

41 where

42+ toTT :: Maybe Type -> PTerm -> StateT Int Idris Term

43+ toTT ty (PRef _ _ n)

36− toTT (PRef _ _ n) = do i <- lift getIState

44+ = do i <- lift getIState

37− case lookupNameDef n (tt_ctxt i) of

45+ case lookupDefExact n (tt_ctxt i) of

38− [(n', TyDecl nt _)] -> return $ P nt n' Erased

46+ Just (TyDecl nt _) -> return $ P nt n Erased

39− _ -> return $ P Ref n Erased

47+ _ -> return $ P Ref n Erased

40− toTT (PApp _ t args) = do t' <- toTT t

48+ toTT ty (PApp _ t@(PRef _ _ n) args)

49+ = do i <- lift getIState

50+ let aTys = case lookupTyExact n (tt_ctxt i) of

51+ Just nty -> map (Just . snd) (getArgTys nty)

52+ Nothing -> map (const Nothing) args

53+ args' <- zipWithM toTT aTys (map getTm args)

54+ t' <- toTT Nothing t

55+ return $ mkApp t' args'

56+ toTT ty (PApp _ t args)

57+ = do t' <- toTT Nothing t

41− args' <- mapM (toTT . getTm) args

58+ args' <- mapM (toTT Nothing . getTm) args

42− return $ mkApp t' args'

59+ return $ mkApp t' args'

43− toTT (PDPair _ _ _ l _ r) = do l' <- toTT l

60+ toTT ty (PDPair _ _ _ l _ r)

61+ = do l' <- toTT Nothing l

44− r' <- toTT r

62+ r' <- toTT Nothing r

45− return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']

63+ return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']

46− toTT (PPair _ _ _ l r) = do l' <- toTT l

64+ toTT ty (PPair _ _ _ l r)

65+ = do l' <- toTT Nothing l

47− r' <- toTT r

66+ r' <- toTT Nothing r

48− return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']

67+ return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']

49 -- For alternatives, pick the first and drop the namespaces. It doesn't

68 -- For alternatives, pick the first and drop the namespaces. It doesn't

50 -- really matter which is taken since matching will ignore the namespace.

69 -- really matter which is taken since matching will ignore the namespace.

51− toTT (PAlternative _ _ (a : as)) = toTT a

70+ toTT (Just ty) (PAlternative _ _ as)

71+ | (hd, _) <- unApply ty

72+ = do i <- lift getIState

73+ case pruneByType True [] hd ty i as of

74+ [a] -> toTT (Just ty) a

75+ _ -> lift $ ierror $ CantResolveAlts (map getAltName as)

76+ toTT Nothing (PAlternative _ _ as)

77+ = lift $ ierror $ CantResolveAlts (map getAltName as)

78+ toTT ty _

52− toTT _ = do v <- get

79+ = do v <- get

53− put (v + 1)

80+ put (v + 1)

54− return (P Bound (sMN v "imp") Erased)

81+ return (P Bound (sMN v "imp") Erased)

55−

82+

56− deNS (PRef f hl (NS n _)) = PRef f hl n

83+ getAltName (PApp _ (PRef _ _ (UN l)) [_, _, arg])

57− deNS t = t

84+ | l == txt "Delay" = getAltName (getTm arg)

85+ getAltName (PApp _ (PRef _ _ n) _) = n

86+ getAltName (PRef _ _ n) = n

87+ getAltName (PApp _ h _) = getAltName h

88+ getAltName (PHidden h) = getAltName h

89+ getAltName x = sUN "_" -- should never happen here

59-- | Given a list of LHSs, generate a extra clauses which cover the remaining

91-- | Given a list of LHSs, generate a extra clauses which cover the remaining

60-- cases. The ones which haven't been provided are marked 'absurd' so

92-- cases. The ones which haven't been provided are marked 'absurd' so

@@ -74,7 +106,9 @@ genClauses fc n lhs_tms given

74 let lhs_given = zipWith removePlaceholders lhs_tms

106 let lhs_given = zipWith removePlaceholders lhs_tms

75 (map (stripUnmatchable i) (map flattenArgs given))

107 (map (stripUnmatchable i) (map flattenArgs given))

108

77− logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))

109+ logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map showTmImpls given)

110+ logCoverage 10 $ "Building coverage tree for:\n" ++ showSep "\n" (map show lhs_given)

111+ logCoverage 10 $ "From terms:\n" ++ showSep "\n" (map show lhs_tms)

78 let givenpos = mergePos (map getGivenPos given)

112 let givenpos = mergePos (map getGivenPos given)

113

80 (cns, ctree_in) <-

114 (cns, ctree_in) <-

src/Idris/Elab/Term.hs+2−163

@@ -1522,7 +1522,7 @@ elab ist info emode opts fn tm

1522 (arg, x : rest)

1523

1524 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]

1525− insertScopedImps fc f knowns ty xs =

1525+ insertScopedImps fc f knowns ty xs =

1526 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs

1527 doInsert ty xs

1528 where

@@ -1538,7 +1538,7 @@ elab ist info emode opts fn tm

1538 = liftM (x :) (doInsert sc xs)

1539 doInsert ty xs = return xs

1540

1541− -- Any implicit in the application needs to have the name of a

1541+ -- Any implicit in the application needs to have the name of a

1542 -- scoped implicit or a top level implicit, otherwise report an error

1543 checkKnownImplicit ns imp@(PImp{})

1544 | pname imp `elem` ns = return ()

@@ -1698,167 +1698,6 @@ pruneAlt xs = map prune xs

1698 headIs f (PApp _ f' _) = headIs f f'

1699 headIs f _ = True -- keep if it's not an application

1700

1701−-- Rule out alternatives that don't return the same type as the head of the goal

1702−-- (If there are none left as a result, do nothing)

1703−pruneByType :: Bool -> Env -> Term -> -- head of the goal

1704− Type -> -- goal

1705− IState -> [PTerm] -> [PTerm]

1706−-- if an alternative has a locally bound name at the head, take it

1707−pruneByType imp env t goalty c as

1708− | Just a <- locallyBound as = [a]

1709− where

1710− locallyBound [] = Nothing

1711− locallyBound (t:ts)

1712− | Just n <- getName t,

1713− n `elem` map fstEnv env = Just t

1714− | otherwise = locallyBound ts

1715− getName (PRef _ _ n) = Just n

1716− getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays

1717− | l == txt "Delay" = getName (getTm arg)

1718− getName (PApp _ f _) = getName f

1719− getName (PHidden t) = getName t

1720− getName _ = Nothing

1721−

1722−-- 'n' is the name at the head of the goal type

1723−pruneByType imp env (P _ n _) goalty ist as

1724−-- if the goal type is polymorphic, keep everything

1725− | Nothing <- lookupTyExact n ctxt = as

1726−-- if the goal type is a ?metavariable, keep everything

1727− | Just _ <- lookup n (idris_metavars ist) = as

1728− | otherwise

1729− = let asV = filter (headIs True n) as

1730− as' = filter (headIs False n) as in

1731− case as' of

1732− [] -> asV

1733− _ -> as'

1734− where

1735− ctxt = tt_ctxt ist

1736−

1737− -- Get the function at the head of the alternative and see if it's

1738− -- a plausible match against the goal type. Keep if so. Also keep if

1739− -- there is a possible coercion to the goal type.

1740− headIs var f (PRef _ _ f') = typeHead var f f'

1741− headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])

1742− | l == txt "Delay" = headIs var f (getTm arg)

1743− headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

1744− headIs var f (PApp _ f' _) = headIs var f f'

1745− headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1746− headIs var f (PHidden t) = headIs var f t

1747− headIs var f t = True -- keep if it's not an application

1748−

1749− typeHead var f f'

1750− = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1751− case lookupTyExact f' ctxt of

1752− Just ty -> case unApply (getRetTy ty) of

1753− (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)

1754− -> False

1755− _ -> let ty' = normalise ctxt [] ty in

1756−-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty

1757−-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $

1758− case unApply (getRetTy ty') of

1759− (V _, _) ->

1760− isPlausible ist var env n ty

1761− _ -> matchingTypes imp (getRetTy ty') goalty

1762− || isCoercion (getRetTy ty') goalty

1763−-- May be useful to keep for debugging purposes for a bit:

1764−-- let res = matching (getRetTy ty') goalty in

1765−-- traceWhen (not res)

1766−-- ("Rejecting " ++ show (getRetTy ty', goalty)) res

1767− _ -> False

1768−

1769− matchingTypes True = matchingHead

1770− matchingTypes False = matching

1771−

1772− -- If the goal is a constructor, it must match the suggested function type

1773− matching (P _ ctyn _) (P _ n' _)

1774− | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'

1775− | otherwise = True

1776− -- Variables match anything

1777− matching (V _) _ = True

1778− matching _ (V _) = True

1779− matching _ (P _ n _) = not (isTConName n ctxt)

1780− matching (P _ n _) _ = not (isTConName n ctxt)

1781− -- Binders are a plausible match, so keep them

1782− matching (Bind n _ sc) _ = True

1783− matching _ (Bind n _ sc) = True

1784− -- If we hit a function name, it's a plausible match

1785− matching apl@(App _ _ _) apr@(App _ _ _)

1786− | (P _ fl _, argsl) <- unApply apl,

1787− (P _ fr _, argsr) <- unApply apr

1788− = fl == fr && and (zipWith matching argsl argsr)

1789− || (not (isConName fl ctxt && isConName fr ctxt))

1790− -- If the application structures aren't easily comparable, it's a

1791− -- plausible match

1792− matching (App _ f a) (App _ f' a') = True

1793− matching (TType _) (TType _) = True

1794− matching (UType _) (UType _) = True

1795− matching l r = l == r

1796−

1797− -- In impossible-case mode, only look at the heads (this is to account for

1798− -- the non type-directed case with 'impossible' - we'd be ruling out

1799− -- too much and wouldn't find the mismatch we're looking for)

1800− matchingHead apl@(App _ _ _) apr@(App _ _ _)

1801− | (P _ fl _, argsl) <- unApply apl,

1802− (P _ fr _, argsr) <- unApply apr,

1803− isConName fl ctxt && isConName fr ctxt

1804− = fl == fr

1805− matchingHead _ _ = True

1806−

1807− -- Return whether there is a possible coercion between the return type

1808− -- of an alternative and the goal type

1809− isCoercion rty gty | (P _ r _, _) <- unApply rty

1810− = not (null (getCoercionsBetween r gty))

1811− isCoercion _ _ = False

1812−

1813− getCoercionsBetween :: Name -> Type -> [Name]

1814− getCoercionsBetween r goal

1815− = let cs = getCoercionsTo ist goal in

1816− findCoercions r cs

1817− where findCoercions t [] = []

1818− findCoercions t (n : ns) =

1819− let ps = case lookupTy n (tt_ctxt ist) of

1820− [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in

1821− [n | any useR as]

1822− _ -> [] in

1823− ps ++ findCoercions t ns

1824−

1825− useR ty =

1826− case unApply (getRetTy ty) of

1827− (P _ t _, _) -> t == r

1828− _ -> False

1829−

1830−

1831−pruneByType _ _ t _ _ as = as

1832−

1833−-- Could the name feasibly be the return type?

1834−-- If there is an interface constraint on the return type, and no implementation

1835−-- in the environment or globally for that name, then no

1836−-- Otherwise, yes

1837−-- (FIXME: This isn't complete, but I'm leaving it here and coming back

1838−-- to it later - just returns 'var' for now. EB)

1839−isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

1840−isPlausible ist var env n ty

1841− = let (hvar, interfaces) = collectConstraints [] [] ty in

1842− case hvar of

1843− Nothing -> True

1844− Just rth -> var -- trace (show (rth, interfaces)) var

1845− where

1846− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1847− (Maybe Name, [(Term, [Name])])

1848− collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)

1849− = let tcs' = case unApply ty of

1850− (P _ c _, _) ->

1851− case lookupCtxtExact c (idris_interfaces ist) of

1852− Just tc -> ((ty, map fst (interface_implementations tc))

1853− : tcs)

1854− Nothing -> tcs

1855− _ -> tcs

1856− in

1857− collectConstraints (n : env) tcs' sc

1858− collectConstraints env tcs t

1859− | (V i, _) <- unApply t = (Just (env !! i), tcs)

1860− | otherwise = (Nothing, tcs)

1861−

1862-- | Use the local elab context to work out the highlighting for a name

1701-- | Use the local elab context to work out the highlighting for a name

1863findHighlight :: Name -> ElabD OutputAnnotation

1702findHighlight :: Name -> ElabD OutputAnnotation

1864findHighlight n = do ctxt <- get_context

1703findHighlight n = do ctxt <- get_context

src/Idris/Elab/Utils.hs+162

@@ -606,4 +606,166 @@ linearArg (Bind n (Pi Rig1 _ _ _) sc) = True

606linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc

607linearArg _ = False

608

609+-- Rule out alternatives that don't return the same type as the head of the goal

610+-- (If there are none left as a result, do nothing)

611+pruneByType :: Bool -> -- In an impossible clause

612+ Env -> Term -> -- head of the goal

613+ Type -> -- goal

614+ IState -> [PTerm] -> [PTerm]

615+-- if an alternative has a locally bound name at the head, take it

616+pruneByType imp env t goalty c as

617+ | Just a <- locallyBound as = [a]

618+ where

619+ locallyBound [] = Nothing

620+ locallyBound (t:ts)

621+ | Just n <- getName t,

622+ n `elem` map fstEnv env = Just t

623+ | otherwise = locallyBound ts

624+ getName (PRef _ _ n) = Just n

625+ getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays

626+ | l == txt "Delay" = getName (getTm arg)

627+ getName (PApp _ f _) = getName f

628+ getName (PHidden t) = getName t

629+ getName _ = Nothing

630+

631+-- 'n' is the name at the head of the goal type

632+pruneByType imp env (P _ n _) goalty ist as

633+-- if the goal type is polymorphic, keep everything

634+ | Nothing <- lookupTyExact n ctxt = as

635+-- if the goal type is a ?metavariable, keep everything

636+ | Just _ <- lookup n (idris_metavars ist) = as

637+ | otherwise

638+ = let asV = filter (headIs True n) as

639+ as' = filter (headIs False n) as in

640+ case as' of

641+ [] -> asV

642+ _ -> as'

643+ where

644+ ctxt = tt_ctxt ist

645+

646+ -- Get the function at the head of the alternative and see if it's

647+ -- a plausible match against the goal type. Keep if so. Also keep if

648+ -- there is a possible coercion to the goal type.

649+ headIs var f (PRef _ _ f') = typeHead var f f'

650+ headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])

651+ | l == txt "Delay" = headIs var f (getTm arg)

652+ headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

653+ headIs var f (PApp _ f' _) = headIs var f f'

654+ headIs var f (PPi _ _ _ _ sc) = headIs var f sc

655+ headIs var f (PHidden t) = headIs var f t

656+ headIs var f t = True -- keep if it's not an application

657+

658+ typeHead var f f'

659+ = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

660+ case lookupTyExact f' ctxt of

661+ Just ty -> case unApply (getRetTy ty) of

662+ (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)

663+ -> False

664+ _ -> let ty' = normalise ctxt [] ty in

665+-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty

666+-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $

667+ case unApply (getRetTy ty') of

668+ (V _, _) ->

669+ isPlausible ist var env n ty

670+ _ -> matchingTypes imp (getRetTy ty') goalty

671+ || isCoercion (getRetTy ty') goalty

672+-- May be useful to keep for debugging purposes for a bit:

673+-- let res = matching (getRetTy ty') goalty in

674+-- traceWhen (not res)

675+-- ("Rejecting " ++ show (getRetTy ty', goalty)) res

676+ _ -> False

677+

678+ matchingTypes True = matchingHead

679+ matchingTypes False = matching

680+

681+ -- If the goal is a constructor, it must match the suggested function type

682+ matching (P _ ctyn _) (P _ n' _)

683+ | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'

684+ | otherwise = True

685+ -- Variables match anything

686+ matching (V _) _ = True

687+ matching _ (V _) = True

688+ matching _ (P _ n _) = not (isTConName n ctxt)

689+ matching (P _ n _) _ = not (isTConName n ctxt)

690+ -- Binders are a plausible match, so keep them

691+ matching (Bind n _ sc) _ = True

692+ matching _ (Bind n _ sc) = True

693+ -- If we hit a function name, it's a plausible match

694+ matching apl@(App _ _ _) apr@(App _ _ _)

695+ | (P _ fl _, argsl) <- unApply apl,

696+ (P _ fr _, argsr) <- unApply apr

697+ = fl == fr && and (zipWith matching argsl argsr)

698+ || (not (isConName fl ctxt && isConName fr ctxt))

699+ -- If the application structures aren't easily comparable, it's a

700+ -- plausible match

701+ matching (App _ f a) (App _ f' a') = True

702+ matching (TType _) (TType _) = True

703+ matching (UType _) (UType _) = True

704+ matching l r = l == r

705+

706+ -- In impossible-case mode, only look at the heads (this is to account for

707+ -- the non type-directed case with 'impossible' - we'd be ruling out

708+ -- too much and wouldn't find the mismatch we're looking for)

709+ matchingHead apl@(App _ _ _) apr@(App _ _ _)

710+ | (P _ fl _, argsl) <- unApply apl,

711+ (P _ fr _, argsr) <- unApply apr,

712+ isConName fl ctxt && isConName fr ctxt

713+ = fl == fr

714+ matchingHead _ _ = True

715+

716+ -- Return whether there is a possible coercion between the return type

717+ -- of an alternative and the goal type

718+ isCoercion rty gty | (P _ r _, _) <- unApply rty

719+ = not (null (getCoercionsBetween r gty))

720+ isCoercion _ _ = False

721+

722+ getCoercionsBetween :: Name -> Type -> [Name]

723+ getCoercionsBetween r goal

724+ = let cs = getCoercionsTo ist goal in

725+ findCoercions r cs

726+ where findCoercions t [] = []

727+ findCoercions t (n : ns) =

728+ let ps = case lookupTy n (tt_ctxt ist) of

729+ [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in

730+ [n | any useR as]

731+ _ -> [] in

732+ ps ++ findCoercions t ns

733+

734+ useR ty =

735+ case unApply (getRetTy ty) of

736+ (P _ t _, _) -> t == r

737+ _ -> False

738+

739+

740+pruneByType _ _ t _ _ as = as

741+

742+-- Could the name feasibly be the return type?

743+-- If there is an interface constraint on the return type, and no implementation

744+-- in the environment or globally for that name, then no

745+-- Otherwise, yes

746+-- (FIXME: This isn't complete, but I'm leaving it here and coming back

747+-- to it later - just returns 'var' for now. EB)

748+isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

749+isPlausible ist var env n ty

750+ = let (hvar, interfaces) = collectConstraints [] [] ty in

751+ case hvar of

752+ Nothing -> True

753+ Just rth -> var -- trace (show (rth, interfaces)) var

754+ where

755+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

756+ (Maybe Name, [(Term, [Name])])

757+ collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)

758+ = let tcs' = case unApply ty of

759+ (P _ c _, _) ->

760+ case lookupCtxtExact c (idris_interfaces ist) of

761+ Just tc -> ((ty, map fst (interface_implementations tc))

762+ : tcs)

763+ Nothing -> tcs

764+ _ -> tcs

765+ in

766+ collectConstraints (n : env) tcs' sc

767+ collectConstraints env tcs t

768+ | (V i, _) <- unApply t = (Just (env !! i), tcs)

769+ | otherwise = (Nothing, tcs)

770+

609

771

test/totality021/expected+4

@@ -3,3 +3,7 @@ Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNot

3totality021.idr:12:1:

4Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

5totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel

6+totality021a.idr:9:1:

7+Main.noNonEmptyPointInt is not total as there are missing cases

8+totality021a.idr:12:1:

9+Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

test/totality021/run+1

@@ -1,3 +1,4 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ totality021.idr --check

3+${IDRIS:-idris} $@ totality021a.idr --check

3rm -f *.ibc

4rm -f *.ibc

test/totality021/totality021a.idrnew file+12

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

1+%default total

3+-- Testing that overloaded names are properly spotted in impossible cases

4+data Point : Nat -> t -> Type where

5+ Nil : Point Z t

6+ (::) : Num t => t -> Point n t -> Point (S n) t

8+noNonEmptyPointInt : (Point (S n) Int) -> Void

9+noNonEmptyPointInt {n} Nil impossible

10+

11+myVoid : Void

12+myVoid = noNonEmptyPointInt [2]