Rakarake/churf
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Change name

Browse source
This commit is contained in:
Martin Fredin 2023-04-24 10:47:33 +02:00
parent 804d0da167
commit 2d96a50219
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/TypeChecker/TypeCheckerBidir.hs
View file

@ -396,13 +396,13 @@ checkPattern patt t_patt = case patt of
-- Γ ⊢ K p₁ p₂ ↑ B ⊣ Δ -- Γ ⊢ K p₁ p₂ ↑ B ⊣ Δ
PInj name ps -> do PInj name ps -> do
t_inj <- maybeToRightM "unknown constructor" =<< lookupInj name t_inj <- maybeToRightM "unknown constructor" =<< lookupInj name
let ps' = getParams t_inj let ts = getParams t_inj
unless (length ps' == length ps) $ unless (length ts' == length ps) $
throwError "Wrong number of arguments!" throwError "Wrong number of arguments!"
sub <- substituteTVarsOf t_inj sub <- substituteTVarsOf t_inj
subtype (sub $ getDataId t_inj) t_patt subtype (sub $ getDataId t_inj) t_patt
let checkP p t = checkPattern p =<< apply (sub t) let checkP p t = checkPattern p =<< apply (sub t)
ps' <- zipWithM checkP ps ps' ps' <- zipWithM checkP ps ts
apply (T.PInj (coerce name) (map fst ps'), t_patt) apply (T.PInj (coerce name) (map fst ps'), t_patt)
where where
substituteTVarsOf = \case substituteTVarsOf = \case