data D : Set where
c : D → {y : D} → D → D
pattern p x {y} z = c x {y} z
f : D → {y : D} → D → D
f = p
Error:
(z : D) → D !=< D
when checking that the expression λ z → p x {y} z has type D
This is already broken in 2.4.2.4 (the oldest Agda I have at my disposal).
Found this bug when reading the code:
A.PatternSyn n -> do (ns, p) <- lookupPatternSyn n p <- return $ setRange (getRange n) $ killRange $ vacuous p -- Pattern' Void -> Pattern' Expr -- Expand the pattern synonym by substituting for -- the arguments we have got and lambda-lifting -- over the ones we haven't. let meta r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r } -- TODO: name suggestion case A.insertImplicitPatSynArgs meta (getRange n) ns args of Nothing -> typeError $ BadArgumentsToPatternSynonym n Just (s, ns) -> do let p' = A.patternToExpr p e' = A.lambdaLiftExpr (map whThing ns) (A.substExpr s p') checkExpr' cmp e' tlambdaLiftExpr
does not take the hiding into account (it is discarded), so the generated lambdas have the wrong hiding.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4