Skip to content

Instantly share code, notes, and snippets.

@cartazio

cartazio/gist:3365312

Created August 16, 2012 01:22
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save cartazio/3365312 to your computer and use it in GitHub Desktop.
Save cartazio/3365312 to your computer and use it in GitHub Desktop.
Download ZIP
more idris ghc 7.6 weird errors
Raw
gistfile1.txt
[20 of 41] Compiling Idris.AbsSyntaxTree ( src/Idris/AbsSyntaxTree.hs, dist/build/idris/idris-tmp/Idris/AbsSyntaxTree.o )
src/Idris/AbsSyntaxTree.hs:622:5:
Could not deduce (Ord a0)
arising from the ambiguity check for `prettyArgS'
from the context (Num a, Ord a)
bound by the inferred type for `prettyArgS':
(Num a, Ord a) => PArg -> Doc
at src/Idris/AbsSyntaxTree.hs:(622,5)-(793,105)
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 b => Ord (Binder b) -- Defined in `Core.TT'
instance Ord Const -- Defined in `Core.TT'
instance Ord Name -- Defined in `Core.TT'
...plus 44 others
When checking that `prettyArgS'
has the inferred type `forall a. (Num a, Ord a) => PArg -> Doc'
Probable cause: the inferred type is ambiguous
In an equation for `prettyImp':
prettyImp impl
= prettySe 10
where
prettySe p (PQuote r)
= if size r > breakingSize then
text "![" $$ pretty r <> text "]"
else
text "![" <> pretty r <> text "]"
prettySe p (PRef fc n)
= if impl then pretty n else prettyBasic n
where
prettyBasic n@(UN _) = pretty n
prettyBasic (MN _ s) = text s
prettyBasic (NS n s)
= (foldr
(<>) empty (intersperse (text ".") (map text $ reverse s)))
<> prettyBasic n
prettySe p (PLam n ty sc)
= bracket p 2
$ if size sc > breakingSize then
text "\955" <> pretty n <+> text "=>" $+$ pretty sc
else
text "\955" <> pretty n <+> text "=>" <+> pretty sc
prettySe p (PLet n ty v sc)
= bracket p 2
$ if size sc > breakingSize then
text "let" <+> pretty n <+> text "=" <+> prettySe 10 v
<+> text "in"
$+$ nest nestingSize (prettySe 10 sc)
else
text "let" <+> pretty n <+> text "=" <+> prettySe 10 v
<+> text "in"
<+> prettySe 10 sc
prettySe p (PPi (Exp l s) n ty sc)
| n `elem` allNamesIn sc || impl
= let ...
in
bracket p 2
$ if size sc > breakingSize then
open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+> st
<+> text "->"
$+$ prettySe 10 sc
else
open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+> st
<+> text "->"
<+> prettySe 10 sc
| otherwise
= bracket p 2
$ if size sc > breakingSize then
prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
else
prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
where
st = ...
prettySe p (PPi (Imp l s) n ty sc)
| impl
= let ...
in
bracket p 2
$ if size sc > breakingSize then
open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+> st
<+> text "->"
<+> prettySe 10 sc
else
open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+> st
<+> text "->"
<+> prettySe 10 sc
| otherwise = prettySe 10 sc
where
st = ...
prettySe p (PPi (Constraint _ _) n ty sc)
= bracket p 2
$ if size sc > breakingSize then
prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
else
prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
prettySe p (PPi (TacImp _ _ s) n ty sc)
= bracket p 2
$ if size sc > breakingSize then
lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty
<> rbrace
<+> text "->"
$+$ prettySe 10 sc
else
lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty
<> rbrace
<+> text "->"
<+> prettySe 10 sc
prettySe p (PApp _ (PRef _ f) []) | not impl = pretty f
prettySe p (PApp _ (PRef _ op@(UN (f : _))) args)
| length (getExps args) == 2 && (not impl) && (not $ isAlpha f)
= let ...
in
bracket p 1
$ if size r > breakingSize then
prettySe 1 l <+> pretty op $+$ prettySe 0 r
else
prettySe 1 l <+> pretty op <+> prettySe 0 r
prettySe p (PApp _ f as)
= let ...
in
bracket p 1
$ prettySe 1 f
<+> if impl then foldl fS empty as else foldl fSe empty args
where
fS l r = ...
fSe l r = ...
prettySe p (PCase _ scr opts)
= text "case" <+> prettySe 10 scr <+> text "of"
$+$ nest nestingSize prettyBody
where
prettyBody
= foldr ($$) empty $ intersperse (text "|") $ map sc opts
sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
prettySe p (PHidden tm) = text "." <> prettySe 0 tm
prettySe p (PRefl _) = text "refl"
prettySe p (PResolveTC _) = text "resolvetc"
prettySe p (PTrue _) = text "()"
prettySe p (PFalse _) = text "_|_"
prettySe p (PEq _ l r)
= bracket p 2
$ if size r > breakingSize then
prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
else
prettySe 10 l <+> text "=" <+> prettySe 10 r
prettySe p (PTyped l r)
= lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
prettySe p (PPair _ l r)
= if size r > breakingSize then
lparen <> prettySe 10 l <> text "," $+$ prettySe 10 r <> rparen
else
lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
prettySe p (PDPair _ l t r)
= if size r > breakingSize then
lparen <> prettySe 10 l <+> text "**" $+$ prettySe 10 r <> rparen
else
lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
prettySe p (PAlternative a as)
= lparen <> text "|" <> prettyAs <> text "|" <> rparen
where
prettyAs = foldr (\ l -> ...) empty $ map (prettySe 10) as
prettySe p PSet = text "Set"
prettySe p (PConstant c) = pretty c
prettySe p (PProof ts)
= text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts)
$+$ rbrace
prettySe p (PTactics ts)
= text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts)
$+$ rbrace
prettySe p (PMetavar n) = text "?" <> pretty n
prettySe p (PReturn f) = text "return"
prettySe p PImpossible = text "impossible"
prettySe p Placeholder = text "_"
prettySe p (PDoBlock _) = text "do block pretty not implemented"
prettySe p (PElabError s) = pretty s
prettySe p _ = text "test"
prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
prettyArgS (PExp _ _ tm) = prettyArgSe tm
prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
prettyArgSe arg = prettySe 0 arg
prettyArgSi (n, val)
= lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
....
src/Idris/AbsSyntaxTree.hs:801:5:
Could not deduce (Ord a0)
arising from the ambiguity check for `seArg'
from the context (Num a, Ord a)
bound by the inferred type for `seArg':
(Num a, Ord a) => PTerm -> [Char]
at src/Idris/AbsSyntaxTree.hs:(801,5)-(874,36)
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 b => Ord (Binder b) -- Defined in `Core.TT'
instance Ord Const -- Defined in `Core.TT'
instance Ord Name -- Defined in `Core.TT'
...plus 44 others
When checking that `seArg'
has the inferred type `forall a. (Num a, Ord a) => PTerm -> [Char]'
Probable cause: the inferred type is ambiguous
In an equation for `showImp':
showImp impl tm
= se 10 tm
where
se p (PQuote r) = "![" ++ show r ++ "]"
se p (PRef fc n)
= if impl then show n else showbasic n
where
showbasic n@(UN _) = show n
showbasic (MN _ s) = s
showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
se p (PLam n ty sc)
= bracket p 2
$ "\\ "
++
show n
++ (if impl then " : " ++ se 10 ty else "") ++ " => " ++ se 10 sc
se p (PLet n ty v sc)
= bracket p 2
$ "let " ++ show n ++ " = " ++ se 10 v ++ " in " ++ se 10 sc
se p (PPi (Exp l s) n ty sc)
| n `elem` allNamesIn sc || impl
= bracket p 2
$ if l then
"|("
else
"("
++ show n ++ " : " ++ se 10 ty ++ ") " ++ st ++ "-> " ++ se 10 sc
| otherwise
= bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
where
st = ...
se p (PPi (Imp l s) n ty sc)
| impl
= bracket p 2
$ if l then
"|{"
else
"{"
++ show n ++ " : " ++ se 10 ty ++ "} " ++ st ++ "-> " ++ se 10 sc
| otherwise = se 10 sc
where
st = ...
se p (PPi (Constraint _ _) n ty sc)
= bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
se p (PPi (TacImp _ _ s) n ty sc)
= bracket p 2
$ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
se p (PApp _ (PRef _ f) []) | not impl = show f
se p (PApp _ (PRef _ op@(UN (f : _))) args)
| length (getExps args) == 2 && not impl && not (isAlpha f)
= let ...
in bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
se p (PApp _ f as)
= let ...
in
bracket p 1
$ se 1 f
++ if impl then concatMap sArg as else concatMap seArg args
se p (PCase _ scr opts)
= "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
where
sc (l, r) = se 10 l ++ " => " ++ se 10 r
se p (PHidden tm) = "." ++ se 0 tm
se p (PRefl _) = "refl"
se p (PResolveTC _) = "resolvetc"
se p (PTrue _) = "()"
se p (PFalse _) = "_|_"
se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
se p (PAlternative a as)
= "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
se p PSet = "Set"
se p (PConstant c) = show c
se p (PProof ts) = "proof { " ++ show ts ++ "}"
se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
se p (PMetavar n) = "?" ++ show n
se p (PReturn f) = "return"
se p PImpossible = "impossible"
se p Placeholder = "_"
se p (PDoBlock _) = "do block show not implemented"
se p (PElabError s) = show s
sArg :: PArg -> [Char]
sArg (PImp _ _ n tm) = siArg (n, tm)
sArg (PExp _ _ tm) = seArg tm
sArg (PConstraint _ _ tm) = scArg tm
sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
seArg arg = " " ++ se 0 arg
....
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment