September 2017 - ghc-tickets

[GHC] #14174: GHC panic with TypeInType and type family
by GHC 10 Jul '18

10 Jul '18

#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This rather simple type family, {{{#!hs {-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-} module GenWhoops where import GHC.Generics type family GenComp k (x :: k) (y :: k) :: Ordering where GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y }}} produces the following panic: {{{ ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170828 for x86_64-unknown-linux): piResultTy k_a1LK[tau:1] p_a1Lz[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type }}} This happens with both GHC 8.2.1 and something very close to HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #12050: Allow haddock comments on non-record types
by GHC 10 Jul '18

10 Jul '18

#12050: Allow haddock comments on non-record types -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 (Parser) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- There are a variety of cases I have found myself wanting to place haddock documentation on fields of non-record data types rather often in the past. The syntax for this might look like, {{{#!hs data Foo = Foo -- ^ A foo Int -- ^ how big is the foo? String -- ^ the name of the foo }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12050> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #8822: Allow -- ^ Haddock syntax on record constructors
by GHC 10 Jul '18

10 Jul '18

#8822: Allow -- ^ Haddock syntax on record constructors -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Parser) | Version: 7.9 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Original ticket is on Haddock Trac [http://trac.haskell.org/haddock/ticket/144 here] which I'm opening here as it requires lexer/parser changes. The idea is that given something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | Branch -- ^ Internal node { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} we'd like it to parse as the user would expect instead of failing. We're currently forced to do something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | -- | Internal node Branch { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} which is quite ugly. I can't think of a reason why the first form wouldn't be allowed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8822> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8
by GHC 10 Jul '18

10 Jul '18

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8 -------------------------------------+------------------------------------- Reporter: cactus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Given the following definitions (just a copy of the relevant bits from sized-types 0.3.5.1, to keep this example self-contained): {{{ -- Copied from sized-types 0.3.5.1 data X0 = X0 data N1 = N1 data X0_ a = X0_ Integer data X1_ a = X1_ Integer type X1 = X1_ X0 type X2 = X0_ (X1_ X0) class Size ix instance Size X0 instance Size a => Size (X1_ a) instance Size a => Size (X0_ a) type family APP0 a type instance APP0 X0 = X0 type instance APP0 N1 = X0_ N1 type instance APP0 (X1_ a) = X0_ (X1_ a) type instance APP0 (X0_ a) = X0_ (X0_ a) type family APP1 a type instance APP1 X0 = X1_ X0 type instance APP1 N1 = N1 type instance APP1 (X1_ a) = X1_ (X1_ a) type instance APP1 (X0_ a) = X1_ (X0_ a) type family SUCC a type instance SUCC X0 = X1_ X0 type instance SUCC N1 = X0 type instance SUCC (X1_ a) = APP0 (SUCC a) type instance SUCC (X0_ a) = APP1 a type family ADD a b type instance ADD a X0 = a type instance ADD X0 a = a type instance ADD X0 N1 = N1 type instance ADD N1 N1 = APP0 N1 type instance ADD N1 (X1_ b) = APP0 b type instance ADD N1 (X0_ b) = APP1 (ADD N1 b) type instance ADD (X1_ a) N1 = APP0 a type instance ADD (X0_ a) N1 = APP1 (ADD a N1) type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X1_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X0_ b) = APP0 (ADD a b) type family NOT a type instance NOT X0 = N1 type instance NOT N1 = X0 type instance NOT (X1_ a) = APP0 (NOT a) type instance NOT (X0_ a) = APP1 (NOT a) type SUB a b = ADD a (SUCC (NOT b)) }}} The following module typechecks with GHC 7.8.3: {{{ data B w = B (&*) :: (Size n, Size n', Size (ADD n' n), n ~ SUB (ADD n' n) n', n' ~ SUB (ADD n' n) n) => [(a, B n)] -> [(b, B n')] -> [((a, b), B (ADD n' n))] mks &* args = undefined foo :: [((), B X1)] foo = [((), B)] bar :: [(((), ()), B X2)] bar = [((), B)] &* foo }}} However, it fails with GHC 7.10.2, with {{{ /tmp/GHCBug.hs:70:7: Couldn't match type ‘ADD X1 n0’ with ‘X0_ (X1_ X0)’ The type variable ‘n0’ is ambiguous Expected type: [(((), ()), B X2)] Actual type: [(((), ()), B (ADD X1 n0))] In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo /tmp/GHCBug.hs:70:17: Occurs check: cannot construct the infinite type: n0 ~ ADD (ADD X1 n0) N1 The type variable ‘n0’ is ambiguous Expected type: SUB (ADD X1 n0) X1 Actual type: n0 In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo Failed, modules loaded: none. }}} The workaround/solution is to change the definition of `bar`: {{{ bar :: [(((), ()), B X2)] bar = [((), B :: B X1)] &* foo }}} This second version typechecks with GHC 7.10.2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11070> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #13109: CUSK improvements
by GHC 10 Jul '18

10 Jul '18

#13109: CUSK improvements -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Inspired by looking at `RnTypes.bindLHsTyVarBndr`, and driven by #11592, Richard and I decided to make some improvements to the treatment of CUSKs. Here's a scrappy Skype dump as a memory-jogger; it is a memory-jogger, not a full description. Richard has notes too {{{ Richard Eisenberg: data F (x :: B a) data G (x :: C b) You have written a complete user-suppled kind signature, but the following variable is undetermined: a0 :: A Perhaps add a kind signature. Inferred kinds of user-written variables: b :: B a0 x :: C b SPJ claim: CUSKs should be handled INDIVIDUALLY and in isoloation, just like term-level type signatures SPJ claim: get rid of the "after the ::" side condition for data types (last bullet of HsDecls Note about CUSKs All of this should mean (SPJ claims) no need for dep_vars returns by bindHsQTyVar, bindLHsTyVarBnrds etc ToDo: clarify comments etc in bindLHStyVarBndr Related to D2914 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13109> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #11282: Injectivity annotation fails in the presence of higher-rank use of constraint family
by GHC 09 Jul '18

09 Jul '18

#11282: Injectivity annotation fails in the presence of higher-rank use of constraint family -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When I say {{{ {-# LANGUAGE TypeFamilies, RankNTypes #-} module Bug where import GHC.Exts type family F a = r | r -> a type family G a :: Constraint meth :: (G a => F a) -> () meth = undefined }}} I get {{{ Bug.hs:10:9: error: • Could not deduce: F a ~ F a0 from the context: G a0 bound by the type signature for: meth :: G a0 => F a0 at Bug.hs:10:9-26 NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘meth’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: meth :: (G a => F a) -> () }}} The presence of `G a` is critical for exhibiting this bug. If I replace `G a` with `Show a` the problem disappears. This one was actually encountered in an attempt to do Useful Work, not just idle typecheckery. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11282> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #12928: Too easy to trigger CUSK condition using TH
by GHC 09 Jul '18

09 Jul '18

#12928: Too easy to trigger CUSK condition using TH -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: feature | Status: new request | Priority: high | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While trying to make `singletons` class promotion work with kind- polymorphic type variables, I've encountered a problem regarding CUSKs. Consider this class: {{{ $(promoteOnly [d| class Cls a where fff :: Proxy a -> () |]) }}} The generated TH (slightly simplified by hand) looks like this: {{{ type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ()) type instance Apply FffSym0 l_alvn = FffSym1 l_alvn class PCls a_alve where type Fff (arg_alvl :: Proxy a_alve) :: () }}} However, it fails to compile with the following error: {{{ cusk.hs:25:1: error: You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature. Inferred kinds of user-written variables: a1627472612 :: k0 l_alvn :: TyFun (Proxy a1627472612) () }}} As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write {{{ data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ()) }}} and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so. Looking at the module `TcHsType` in the GHC sources, I see that the error is reported by the `kcHsTyVarBndrs` function: {{{ -- If there are any meta-tvs left, the user has -- lied about having a CUSK. Error. ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs ; when (not (null meta_tvs)) $ report_non_cusk_tvs (qkvs ++ tc_tvs) }}} However, I don't see why we can't generalize over `meta_tvs` instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound. Below I attach a self-contained example that demonstrates the issue and has no dependencies except `base`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12928> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #14091: When PolyKinds is on, suggested type signatures seem to require TypeInType
by GHC 09 Jul '18

09 Jul '18

#14091: When PolyKinds is on, suggested type signatures seem to require TypeInType -------------------------------------+------------------------------------- Reporter: jberryman | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- We compile the following with -Wall {{{ {-# LANGUAGE PolyKinds #-} import Data.Bits import Data.Word data Hash128 a = Hash128 { hashWord128_0 :: !Word64, hashWord128_1 :: !Word64 } deriving (Show, Read, Eq) -- These instances copied from 'FixedPoint-simple': instance FiniteBits (Hash128 a) where finiteBitSize ~(Hash128 a b) = finiteBitSize a + finiteBitSize b instance Bits (Hash128 a) where popCount (Hash128 h l) = popCount h + popCount l bit i | i >= 64 = Hash128 (bit $ i - 64) 0 | otherwise = Hash128 0 (bit i) complement = pointwise complement (.&.) = pointwise2 (.&.) (.|.) = pointwise2 (.|.) xor = pointwise2 xor setBit (Hash128 h l) i | i >= 64 = Hash128 (setBit h (i - 64)) l | otherwise = Hash128 h (setBit l i) shiftL (Hash128 h l) i | i > finiteBitSize l = shiftL (Hash128 l 0) (i - finiteBitSize l) | otherwise = Hash128 ((h `shiftL` i) .|. (l `shiftR` (finiteBitSize l - i))) (l `shiftL` i) shiftR (Hash128 h l) i | i > finiteBitSize h = shiftR (Hash128 0 h) (i - finiteBitSize h) | otherwise = Hash128 (h `shiftR` i) ((l `shiftR` i) .|. h `shiftL` (finiteBitSize h - i)) isSigned _ = False testBit (Hash128 h l) i | i >= finiteBitSize l = testBit h (i - finiteBitSize l) | otherwise = testBit l i rotateL w i = shiftL w i .|. shiftR w (128 - i) rotateR w i = shiftR w i .|. shiftL w (128 - i) bitSize _ = 128 bitSizeMaybe _ = Just 128 pointwise op (Hash128 a b) = Hash128 (op a) (op b) pointwise2 op (Hash128 a b) (Hash128 c d) = Hash128 (op a c) (op b d) }}} get a warning like: {{{ Top-level binding with no type signature: pointwise2 :: forall k1 k2 k3 (a1 :: k2) (a2 :: k1) (a3 :: k3). (Word64 -> Word64 -> Word64) -> Hash128 a1 -> Hash128 a2 -> Hash128 a3 }}} but that's not a valid signature. Pasting it in causes GHC to suggest RankNTypes with an error, and then to suggest TypeInType, at which point it compiles. I want to just be able to paste in the signature from the warning. Related to #6065 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14091> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #9123: Need for higher kinded roles
by GHC 08 Jul '18

08 Jul '18

#9123: Need for higher kinded roles ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`! In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used. This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9123> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 66

[GHC] #9672: Error message too long (full case statement printed)
by GHC 06 Jul '18

06 Jul '18

#9672: Error message too long (full case statement printed) -------------------------------------+------------------------------------- Reporter: andreas.abel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Other Difficulty: Easy (less than 1 | Test Case: hour) | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Imho, it does not make sense to print the other branches of a case when a type error is discovered in one branch. When you see the following example, you will agree with me. {{{ src/full/Agda/TypeChecking/Errors.hs:540:35: Couldn't match type ‘[Char]’ with ‘TCMT IO Doc’ Expected type: TCM Doc Actual type: [Char] In the expression: "Module cannot be imported since it has open interaction points" In a case alternative: SolvedButOpenHoles -> "Module cannot be imported since it has open interaction points" In a stmt of a 'do' block: }}} {{{#!hs case err of { InternalError s -> panic s NotImplemented s -> fwords $ "Not implemented: " ++ s NotSupported s -> fwords $ "Not supported: " ++ s CompilationError s -> sep [fwords "Compilation error:", text s] GenericError s -> fwords s GenericDocError d -> return d TerminationCheckFailed because -> fwords "Termination checking failed for the following functions:" $$ (nest 2 $ fsep $ punctuate comma $ map (pretty . dropTopLevelModule) $ concatMap termErrFunctions because) $$ fwords "Problematic calls:" $$ (nest 2 $ fmap (P.vcat . nub) $ mapM prettyTCM $ sortBy (compare `on` callInfoRange) $ concatMap termErrCalls because) PropMustBeSingleton -> fwords "Datatypes in Prop must have at most one constructor when proof irrelevance is enabled" DataMustEndInSort t -> fsep $ pwords "The type of a datatype must end in a sort." ++ [prettyTCM t] ++ pwords "isn't a sort." ShouldEndInApplicationOfTheDatatype t -> fsep $ pwords "The target of a constructor must be the datatype applied to its parameters," ++ [prettyTCM t] ++ pwords "isn't" ShouldBeAppliedToTheDatatypeParameters s t -> fsep $ pwords "The target of the constructor should be" ++ [prettyTCM s] ++ pwords "instead of" ++ [prettyTCM t] ShouldBeApplicationOf t q -> fsep $ pwords "The pattern constructs an element of" ++ [prettyTCM q] ++ pwords "which is not the right datatype" ShouldBeRecordType t -> fsep $ pwords "Expected non-abstract record type, found " ++ [prettyTCM t] ShouldBeRecordPattern p -> fsep $ pwords "Expected record pattern" NotAProjectionPattern p -> fsep $ pwords "Not a valid projection for a copattern: " ++ [prettyA p] DifferentArities -> fwords "The number of arguments in the defining equations differ" WrongHidingInLHS -> do { fwords "Unexpected implicit argument" } WrongHidingInLambda t -> do { fwords "Found an implicit lambda where an explicit lambda was expected" } WrongIrrelevanceInLambda t -> do { fwords "Found an irrelevant lambda where a relevant lambda was expected" } WrongNamedArgument a -> fsep $ pwords "Function does not accept argument " ++ [prettyTCM a] WrongHidingInApplication t -> do { fwords "Found an implicit application where an explicit application was expected" } HidingMismatch h h' -> fwords $ "Expected " ++ verbalize (Indefinite h') ++ " argument, but found " ++ verbalize (Indefinite h) ++ " argument" RelevanceMismatch r r' -> fwords $ "Expected " ++ verbalize (Indefinite r') ++ " argument, but found " ++ verbalize (Indefinite r) ++ " argument" ColorMismatch c c' -> fsep $ pwords "Expected argument color to be" ++ [prettyTCM c'] ++ pwords "but found color" ++ [prettyTCM c] NotInductive t -> fsep $ [prettyTCM t] ++ pwords "is not an inductive data type" UninstantiatedDotPattern e -> fsep $ pwords "Failed to infer the value of dotted pattern" IlltypedPattern p a -> fsep $ pwords "Type mismatch" IllformedProjectionPattern p -> fsep $ pwords "Ill-formed projection pattern " ++ [prettyA p] CannotEliminateWithPattern p a -> do { let ...; fsep $ pwords "Cannot eliminate type" ++ prettyTCM a : if isProj then pwords "with projection pattern" ++ ... else pwords "with pattern" ++ prettyA p : pwords "(did you supply too many arguments?)" } TooManyArgumentsInLHS a -> fsep $ pwords "Left hand side gives too many arguments to a function of type" ++ [prettyTCM a] WrongNumberOfConstructorArguments c expect given -> fsep $ pwords "The constructor" ++ [prettyTCM c] ++ pwords "expects" ++ [text (show expect)] ++ pwords "arguments (including hidden ones), but has been given" ++ [text (show given)] ++ pwords "(including hidden ones)" CantResolveOverloadedConstructorsTargetingSameDatatype d cs -> fsep $ pwords ("Can't resolve overloaded constructors targeting the same datatype (" ++ show (qnameToConcrete d) ++ "):") ++ map pretty cs DoesNotConstructAnElementOf c t -> fsep $ pwords "The constructor" ++ [prettyTCM c] ++ pwords "does not construct an element of" ++ [prettyTCM t] ConstructorPatternInWrongDatatype c d -> fsep $ [prettyTCM c] ++ pwords "is not a constructor of the datatype" ++ [prettyTCM d] IndicesNotConstructorApplications [i] -> fwords "The index" $$ nest 2 (prettyTCM i) $$ fsep (pwords "is not a constructor (or literal) applied to variables" ++ pwords "(note that parameters count as constructor arguments)") IndicesNotConstructorApplications is -> fwords "The indices" $$ nest 2 (vcat $ map prettyTCM is) $$ fsep (pwords "are not constructors (or literals) applied to variables" ++ pwords "(note that parameters count as constructor arguments)") IndexVariablesNotDistinct vs is -> fwords "The variables" $$ nest 2 (vcat $ map (\ v -> prettyTCM (I.Var v [])) vs) $$ fwords "in the indices" $$ nest 2 (vcat $ map prettyTCM is) $$ fwords "are not distinct (note that parameters count as constructor arguments)" IndicesFreeInParameters vs indices pars -> fwords "The variables" $$ nest 2 (vcat $ map (\ v -> prettyTCM (I.Var v [])) vs) $$ fwords "which are used (perhaps as constructor parameters) in the index expressions" $$ nest 2 (vcat $ map prettyTCM indices) $$ fwords "are free in the parameters" $$ nest 2 (vcat $ map prettyTCM pars) ShadowedModule x [] -> (throwImpossible (Impossible "src/full/Agda/TypeChecking/Errors.hs" 404)) ShadowedModule x ms@(m : _) -> fsep $ pwords "Duplicate definition of module" ++ [prettyTCM x <> text "."] ++ pwords "Previous definition of" ++ [help m] ++ pwords "module" ++ [prettyTCM x] ++ pwords "at" ++ [prettyTCM r] where help m = do { ... } r = case ... of { [] -> ... r : _ -> ... } defSiteOfLast [] = noRange defSiteOfLast ns = nameBindingSite (last ns) ModuleArityMismatch m EmptyTel args -> fsep $ pwords "The module" ++ [prettyTCM m] ++ pwords "is not parameterized, but is being applied to arguments" ModuleArityMismatch m tel@(ExtendTel _ _) args -> fsep $ pwords "The arguments to " ++ [prettyTCM m] ++ pwords "does not fit the telescope" ++ [prettyTCM tel] ShouldBeEmpty t [] -> fsep $ [prettyTCM t] ++ pwords "should be empty, but that's not obvious to me" ShouldBeEmpty t ps -> fsep ([prettyTCM t] ++ pwords "should be empty, but the following constructor patterns are valid:") $$ nest 2 (vcat $ map (showPat 0) ps) ShouldBeASort t -> fsep $ [prettyTCM t] ++ pwords "should be a sort, but it isn't" ShouldBePi t -> fsep $ [prettyTCM t] ++ pwords "should be a function type, but it isn't" NotAProperTerm -> fwords "Found a malformed term" SetOmegaNotValidType -> fwords "Set\969 is not a valid type" InvalidType v -> fsep $ [prettyTCM v] ++ pwords "is not a valid type" SplitOnIrrelevant p t -> fsep $ pwords "Cannot pattern match" ++ [prettyA p] ++ pwords "against irrelevant type" ++ [prettyTCM t] DefinitionIsIrrelevant x -> fsep $ text "Identifier" : prettyTCM x : pwords "is declared irrelevant, so it cannot be used here" VariableIsIrrelevant x -> fsep $ text "Variable" : prettyTCM x : pwords "is declared irrelevant, so it cannot be used here" UnequalBecauseOfUniverseConflict cmp s t -> fsep $ [prettyTCM s, notCmp cmp, ....] UnequalTerms cmp s t a -> do { (d1, d2, d) <- prettyInEqual s t; fsep $ [...] ++ pwords "of type" ++ [...] ++ [...] } UnequalTypes cmp a b -> prettyUnequal a (notCmp cmp) b UnequalColors a b -> error "TODO guilhem 4" HeterogeneousEquality u a v b -> fsep $ pwords "Refuse to solve heterogeneous constraint" ++ [prettyTCM u] ++ pwords ":" ++ [prettyTCM a] ++ pwords "=?=" ++ [prettyTCM v] ++ pwords ":" ++ [prettyTCM b] UnequalRelevance cmp a b -> fsep $ [prettyTCM a, notCmp cmp, ....] ++ pwords "because one is a relevant function type and the other is an irrelevant function type" UnequalHiding a b -> fsep $ [prettyTCM a, text "!=", ....] ++ pwords "because one is an implicit function type and the other is an explicit function type" UnequalSorts s1 s2 -> fsep $ [prettyTCM s1, text "!=", ....] NotLeqSort s1 s2 -> fsep $ pwords "The type of the constructor does not fit in the sort of the datatype, since" ++ [prettyTCM s1] ++ pwords "is not less or equal than" ++ [prettyTCM s2] TooFewFields r xs -> fsep $ pwords "Missing fields" ++ punctuate comma (map pretty xs) ++ pwords "in an element of the record" ++ [prettyTCM r] TooManyFields r xs -> fsep $ pwords "The record type" ++ [prettyTCM r] ++ pwords "does not have the fields" ++ punctuate comma (map pretty xs) DuplicateConstructors xs -> fsep $ pwords "Duplicate constructors" ++ punctuate comma (map pretty xs) ++ pwords "in datatype" DuplicateFields xs -> fsep $ pwords "Duplicate fields" ++ punctuate comma (map pretty xs) ++ pwords "in record" UnexpectedWithPatterns ps -> fsep $ pwords "Unexpected with patterns" ++ (punctuate (text " |") $ map prettyA ps) WithClausePatternMismatch p q -> fsep $ pwords "With clause pattern " ++ [prettyA p] ++ pwords " is not an instance of its parent pattern " ++ [prettyTCM q] MetaCannotDependOn m ps i -> fsep $ pwords "The metavariable" ++ [prettyTCM $ MetaV m []] ++ pwords "cannot depend on" ++ [pvar i] ++ pwords "because it" ++ deps where pvar = prettyTCM . var deps = case map pvar ps of { [] -> ... [x] -> ... xs -> ... } MetaOccursInItself m -> fsep $ pwords "Cannot construct infinite solution of metavariable" ++ [prettyTCM $ MetaV m []] BuiltinMustBeConstructor s e -> fsep $ [prettyA e] ++ pwords "must be a constructor in the binding to builtin" ++ [text s] NoSuchBuiltinName s -> fsep $ pwords "There is no built-in thing called" ++ [text s] DuplicateBuiltinBinding b x y -> fsep $ pwords "Duplicate binding for built-in thing" ++ [text b <> comma] ++ pwords "previous binding to" ++ [prettyTCM x] NoBindingForBuiltin x -> fsep $ pwords "No binding for builtin thing" ++ [text x <> comma] ++ pwords ("use {-# BUILTIN " ++ x ++ " name #-} to bind it to 'name'") NoSuchPrimitiveFunction x -> fsep $ pwords "There is no primitive function called" ++ [text x] BuiltinInParameterisedModule x -> fwords $ "The BUILTIN pragma cannot appear inside a bound context " ++ "(for instance, in a parameterised module or as a local declaration)" IllegalLetInTelescope tb -> fsep $ [pretty tb] ++ pwords " is not allowed in a telescope here." NoRHSRequiresAbsurdPattern ps -> fwords $ "The right-hand side can only be omitted if there " ++ "is an absurd pattern, () or {}, in the left-hand side." AbsurdPatternRequiresNoRHS ps -> fwords $ "The right-hand side must be omitted if there " ++ "is an absurd pattern, () or {}, in the left-hand side." LocalVsImportedModuleClash m -> fsep $ pwords "The module" ++ [text $ show m] ++ pwords "can refer to either a local module or an imported module" SolvedButOpenHoles -> "Module cannot be imported since it has open interaction points" UnsolvedMetas rs -> fsep (pwords "Unsolved metas at the following locations:") $$ nest 2 (vcat $ map prettyTCM rs) UnsolvedConstraints cs -> fsep (pwords "Failed to solve the following constraints:") $$ nest 2 (vcat $ map prettyConstraint cs) where prettyConstraint :: ProblemConstraint -> TCM Doc prettyConstraint c = f (prettyTCM c) where r = ... .... CyclicModuleDependency ms -> fsep (pwords "cyclic module dependency:") $$ nest 2 (vcat $ map pretty ms) FileNotFound x files -> fsep (pwords "Failed to find source of module" ++ [pretty x] ++ pwords "in any of the following locations:") $$ nest 2 (vcat $ map (text . filePath) files) OverlappingProjects f m1 m2 -> fsep (pwords "The file" ++ [text (filePath f)] ++ pwords "can be accessed via several project roots. Both" ++ [pretty m1] ++ pwords "and" ++ [pretty m2] ++ pwords "point to this file.") AmbiguousTopLevelModuleName x files -> fsep (pwords "Ambiguous module name. The module name" ++ [pretty x] ++ pwords "could refer to any of the following files:") $$ nest 2 (vcat $ map (text . filePath) files) ClashingFileNamesFor x files -> fsep (pwords "Multiple possible sources for module" ++ [text $ show x] ++ pwords "found:") $$ nest 2 (vcat $ map (text . filePath) files) ModuleDefinedInOtherFile mod file file' -> fsep $ pwords "You tried to load" ++ [text (filePath file)] ++ pwords "which defines the module" ++ [pretty mod <> text "."] ++ pwords "However, according to the include path this module should" ++ pwords "be defined in" ++ [text (filePath file') <> text "."] ModuleNameDoesntMatchFileName given files -> fsep (pwords "The name of the top level module does not match the file name. The module" ++ [pretty given] ++ pwords "should be defined in one of the following files:") $$ nest 2 (vcat $ map (text . filePath) files) BothWithAndRHS -> fsep $ pwords "Unexpected right hand side" NotInScope xs -> fsep (pwords "Not in scope:") $$ nest 2 (vcat $ map name xs) where name x = fsep [...] suggestion s | elem ':' s = parens $ text "did you forget space around the ':'?" | elem "->" two = parens $ text "did you forget space around the '->'?" | otherwise = empty where two = ... NoSuchModule x -> fsep $ pwords "No such module" ++ [pretty x] AmbiguousName x ys -> vcat [fsep $ pwords "Ambiguous name" ++ [...] ++ pwords "It could refer to any one of", nest 2 $ vcat $ map nameWithBinding ys, ....] AmbiguousModule x ys -> vcat [fsep $ pwords "Ambiguous module name" ++ [...] ++ pwords "It could refer to any one of", nest 2 $ vcat $ map help ys, ....] where help :: ModuleName -> TCM Doc help m = do { ... } UninstantiatedModule x -> fsep (pwords "Cannot access the contents of the parameterised module" ++ [pretty x <> text "."] ++ pwords "To do this the module first has to be instantiated. For instance:") $$ nest 2 (hsep [text "module", pretty x <> text "'", ....]) ClashingDefinition x y -> fsep $ pwords "Multiple definitions of" ++ [pretty x <> text "."] ++ pwords "Previous definition at" ++ [prettyTCM $ nameBindingSite $ qnameName y] ClashingModule m1 m2 -> fsep $ pwords "The modules" ++ [prettyTCM m1, text "and", ....] ++ pwords "clash." ClashingImport x y -> fsep $ pwords "Import clash between" ++ [pretty x, text "and", ....] ClashingModuleImport x y -> fsep $ pwords "Module import clash between" ++ [pretty x, text "and", ....] PatternShadowsConstructor x c -> fsep $ pwords "The pattern variable" ++ [prettyTCM x] ++ pwords "has the same name as the constructor" ++ [prettyTCM c] DuplicateImports m xs -> fsep $ pwords "Ambiguous imports from module" ++ [pretty m] ++ pwords "for" ++ punctuate comma (map pretty xs) ModuleDoesntExport m xs -> fsep $ pwords "The module" ++ [pretty m] ++ pwords "doesn't export the following:" ++ punctuate comma (map pretty xs) NotAModuleExpr e -> fsep $ pwords "The right-hand side of a module definition must have the form 'M e1 .. en'" ++ pwords "where M is a module name. The expression" ++ [pretty e, text "doesn't."] FieldOutsideRecord -> fsep $ pwords "Field appearing outside record declaration." InvalidPattern p -> fsep $ pretty p : pwords "is not a valid pattern" RepeatedVariablesInPattern xs -> fsep $ pwords "Repeated variables in left hand side:" ++ map pretty xs NotAnExpression e -> fsep $ [pretty e] ++ pwords "is not a valid expression." NotAValidLetBinding nd -> fwords $ "Not a valid let-declaration" NothingAppliedToHiddenArg e -> fsep $ [pretty e] ++ pwords "cannot appear by itself. It needs to be the argument to" ++ pwords "a function expecting an implicit argument." NothingAppliedToInstanceArg e -> fsep $ [pretty e] ++ pwords "cannot appear by itself. It needs to be the argument to" ++ pwords "a function expecting an instance argument." NoParseForApplication es -> fsep $ pwords "Could not parse the application" ++ [pretty $ C.RawApp noRange es] AmbiguousParseForApplication es es' -> fsep (pwords "Don't know how to parse" ++ [pretty_es <> (text ".")] ++ pwords "Could mean any one of:") $$ nest 2 (vcat $ map pretty' es') where pretty_es :: TCM Doc pretty_es = pretty $ C.RawApp noRange es pretty' :: C.Expr -> TCM Doc .... BadArgumentsToPatternSynonym x -> fsep $ pwords "Bad arguments to pattern synonym " ++ [prettyTCM x] TooFewArgumentsToPatternSynonym x -> fsep $ pwords "Too few arguments to pattern synonym " ++ [prettyTCM x] UnusedVariableInPatternSynonym -> fsep $ pwords "Unused variable in pattern synonym." NoParseForLHS IsLHS p -> fsep $ pwords "Could not parse the left-hand side" ++ [pretty p] NoParseForLHS IsPatSyn p -> fsep $ pwords "Could not parse the pattern synonym" ++ [pretty p] AmbiguousParseForLHS lhsOrPatSyn p ps -> fsep (pwords "Don't know how to parse" ++ [pretty_p <> text "."] ++ pwords "Could mean any one of:") $$ nest 2 (vcat $ map pretty' ps) where pretty_p :: TCM Doc pretty_p = pretty p pretty' :: C.Pattern -> TCM Doc .... IncompletePatternMatching v args -> fsep $ pwords "Incomplete pattern matching for" ++ [prettyTCM v <> text "."] ++ pwords "No match for" ++ map prettyTCM args UnreachableClauses f pss -> fsep $ pwords "Unreachable" ++ pwords (plural (length pss) "clause") where plural 1 thing = thing plural n thing = thing ++ "s" CoverageFailure f pss -> fsep (pwords "Incomplete pattern matching for" ++ [prettyTCM f <> text "."] ++ pwords "Missing cases:") $$ nest 2 (vcat $ map display pss) where display ps = do { ... } nicify f ps = do { ... } CoverageCantSplitOn c tel cIxs gIxs | length cIxs /= length gIxs -> (throwImpossible (Impossible "src/full/Agda/TypeChecking/Errors.hs" 750)) | otherwise -> addCtxTel tel $ vcat ([fsep $ pwords "I'm not sure if there should be a case for the constructor" ++ [...] ++ pwords "because I get stuck when trying to solve the following" ++ pwords "unification problems (inferred index \8799 expected index):"] ++ zipWith (\ c g -> nest 2 $ prettyTCM c <+> text "\8799" <+> prettyTCM g) cIxs gIxs) CoverageCantSplitIrrelevantType a -> fsep $ pwords "Cannot split on argument of irrelevant datatype" ++ [prettyTCM a] CoverageCantSplitType a -> fsep $ pwords "Cannot split on argument of non-datatype" ++ [prettyTCM a] SplitError e -> prettyTCM e WithoutKError a u v -> fsep $ pwords "Cannot eliminate reflexive equation" ++ [prettyTCM u] ++ pwords "=" ++ [prettyTCM v] ++ pwords "of type" ++ [prettyTCM a] ++ pwords "because K has been disabled." NotStrictlyPositive d ocs -> fsep $ pwords "The datatype" ++ [prettyTCM d] ++ pwords "is not strictly positive, because" ++ prettyOcc "it" ocs where prettyOcc _ [] = [] prettyOcc it (OccCon d c r : ocs) = concat [...] prettyOcc it (OccClause f n r : ocs) = concat [...] prettyR NonPositively = pwords "negatively" prettyR (ArgumentTo i q) = pwords "as the" ++ [...] ++ pwords "argument to" ++ [...] th 0 = text "first" th 1 = text "second" th 2 = text "third" th n = text (show $ n - 1) <> text "th" .... IFSNoCandidateInScope t -> fsep $ pwords "No variable of type" ++ [prettyTCM t] ++ pwords "was found in scope." SafeFlagPostulate e -> fsep $ pwords "Cannot postulate" ++ [pretty e] ++ pwords "with safe flag" SafeFlagPragma xs -> let plural | length xs == 1 = ... | otherwise = ... in fsep $ [fwords ("Cannot set OPTION pragma" ++ plural)] ++ map text xs ++ [fwords "with safe flag."] SafeFlagNoTerminationCheck -> fsep (pwords "Cannot use NO_TERMINATION_CHECK pragma with safe flag.") SafeFlagNonTerminating -> fsep (pwords "Cannot use NON_TERMINATING pragma with safe flag.") SafeFlagTerminating -> fsep (pwords "Cannot use TERMINATING pragma with safe flag.") SafeFlagPrimTrustMe -> fsep (pwords "Cannot use primTrustMe with safe flag") NeedOptionCopatterns -> fsep (pwords "Option --copatterns needed to enable destructor patterns") } }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9672> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8