Skip to content

@cartazio /gist:3405712
Created

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
idris install error
carter ~ » cabal install idris
Resolving dependencies...
[1 of 1] Compiling Main ( /var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.2.1-1497/idris-0.9.2.1/Setup.hs, /var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.2.1-1497/idris-0.9.2.1/dist/setup/Main.o )
Linking /var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.2.1-1497/idris-0.9.2.1/dist/setup/setup ...
Configuring idris-0.9.2.1...
Building idris-0.9.2.1...
Preprocessing executable 'idris' for idris-0.9.2.1...
[ 1 of 32] Compiling Util.Pretty ( src/Util/Pretty.hs, dist/build/idris/idris-tmp/Util/Pretty.o )
[ 2 of 32] Compiling Core.TT ( src/Core/TT.hs, dist/build/idris/idris-tmp/Core/TT.o )
src/Core/TT.hs:614:5:
Could not deduce (Ord a0)
arising from the ambiguity check for `prettySb'
from the context (Eq a1, Num a, Ord a, Show a1, Pretty a1)
bound by the inferred type for `prettySb':
(Eq a1, Num a, Ord a, Show a1, Pretty a1) =>
[(a1, Binder (TT a1))] -> a1 -> Binder (TT a1) -> Bool -> Doc
at src/Core/TT.hs:(614,5)-(651,42)
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there are several potential instances:
instance Ord Name -- Defined at src/Core/TT.hs:152:17
instance Ord UExp -- Defined at src/Core/TT.hs:346:17
instance Integral a => Ord (GHC.Real.Ratio a)
-- Defined in `GHC.Real'
...plus 28 others
When checking that `prettySb'
has the inferred type `forall a a1.
(Eq a1, Num a, Ord a, Show a1, Pretty a1) =>
[(a1, Binder (TT a1))] -> a1 -> Binder (TT a1) -> Bool -> Doc'
Probable cause: the inferred type is ambiguous
In an equation for `prettyEnv':
prettyEnv env t
= prettyEnv' env t False
where
prettyEnv' env t dbg = prettySe 10 env t dbg
bracket outer inner p
| inner > outer = lparen <> p <> rparen
| otherwise = p
prettySe p env (P nt n t) debug
= pretty n
<+>
if debug then
lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug
<+> rbrack
else
empty
prettySe p env (V i) debug
| i < length env
= if debug then
text . show . fst $ env !! i
else
lbrack <+> text (show i) <+> rbrack
| otherwise = text "unbound" <+> text (show i) <+> text "!"
prettySe p env (Bind n b@(Pi t) sc) debug
| noOccurrence n sc && not debug
= bracket p 2
$ prettySb env n b debug <> prettySe 10 ((n, b) : env) sc debug
prettySe p env (Bind n b sc) debug
= bracket p 2
$ prettySb env n b debug <> prettySe 10 ((n, b) : env) sc debug
prettySe p env (App f a) debug
= bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
prettySe p env (Constant c) debug = pretty c
prettySe p env Erased debug = text "[_]"
prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
prettySb env n (Lam t) = prettyB env "\955" "=>" n t
prettySb env n (Hole t) = prettyB env "?defer" "." n t
prettySb env n (Pi t) = prettyB env "(" ") ->" n t
prettySb env n (PVar t) = prettyB env "pat" "." n t
prettySb env n (PVTy t) = prettyB env "pty" "." n t
prettySb env n (Let t v) = prettyBv env "let" "in" n t v
prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
....
src/Core/TT.hs:655:5:
Could not deduce (Ord a0) arising from the ambiguity check for `sb'
from the context (Eq a1, Num a, Ord a, Show a1)
bound by the inferred type for `sb':
(Eq a1, Num a, Ord a, Show a1) =>
[(a1, Binder (TT a1))] -> a1 -> Binder (TT a1) -> [Char]
at src/Core/TT.hs:(655,5)-(679,46)
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there are several potential instances:
instance Ord Name -- Defined at src/Core/TT.hs:152:17
instance Ord UExp -- Defined at src/Core/TT.hs:346:17
instance Integral a => Ord (GHC.Real.Ratio a)
-- Defined in `GHC.Real'
...plus 28 others
When checking that `sb'
has the inferred type `forall a a1.
(Eq a1, Num a, Ord a, Show a1) =>
[(a1, Binder (TT a1))] -> a1 -> Binder (TT a1) -> [Char]'
Probable cause: the inferred type is ambiguous
In an equation for showEnv':
showEnv' env t dbg
= se 10 env t
where
se p env (P nt n t)
= show n
++
if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
se p env (V i)
| i < length env
= (show $ fst $ env !! i)
++ if dbg then "{" ++ show i ++ "}" else ""
| otherwise = "!!V " ++ show i ++ "!!"
se p env (Bind n b@(Pi t) sc)
| noOccurrence n sc && not dbg
= bracket p 2 $ se 1 env t ++ " -> " ++ se 10 ((n, b) : env) sc
se p env (Bind n b sc)
= bracket p 2 $ sb env n b ++ se 10 ((n, b) : env) sc
se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
se p env (Constant c) = show c
se p env Erased = "[__]"
se p env (Set i) = "Set " ++ show i
sb env n (Lam t) = showb env "\\ " " => " n t
sb env n (Hole t) = showb env "? " ". " n t
sb env n (GHole t) = showb env "?defer " ". " n t
sb env n (Pi t) = showb env "(" ") -> " n t
sb env n (PVar t) = showb env "pat " ". " n t
sb env n (PVTy t) = showb env "pty " ". " n t
sb env n (Let t v) = showbv env "let " " in " n t v
sb env n (Guess t v) = showbv env "?? " " in " n t v
showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
showbv env op sc n t v
= op
++ show n ++ " : " ++ se 10 env t ++ " = " ++ se 10 env v ++ sc
....
cabal: Error: some packages failed to install:
idris-0.9.2.1 failed during the building phase. The exception was:
ExitFailure 1
carter ~ »
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.