@@ -385,12 +385,17 @@ tcRho scope c (Reset ctl t) mb_ty =
385385 case ty of
386386 VApp c id [] -> return (Reset (Coordination mb_mn conj (snd id )) t, ty)
387387 _ -> evalError (pp " Needs atomic type" <+> ppValue Unqualified 0 ty)
388- tcRho scope s (Opts n cs) mb_ty = do
388+ tcRho scope s (Opts (nty,n) cs) mb_ty = do
389+ gl <- globals
389390 let (s1,s2,s3) = split3 s
390- (n,_) <- tcRho scope s1 n Nothing
391- (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
391+ (n,nty) <- tcRho scope s1 n (nty <&> \ ty -> eval gl [] poison ty [] )
392+ nty <- value2termM True [] nty
393+ ls <- forCM s2 cs $ \ s' ((lty,l),_) -> do
394+ (l,lty) <- tcRho scope s' l (lty <&> \ ty -> eval gl [] poison ty [] )
395+ lty <- value2termM True [] lty
396+ return (Just lty, l)
392397 (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
393- return (Opts n (zip ls ts), ty)
398+ return (Opts ( Just nty, n) (zip ls ts), ty)
394399tcRho scope s t _ = unimplemented (" tcRho " ++ show t)
395400
396401evalCodomain :: Scope -> Ident -> Value -> EvalM Value
@@ -1110,9 +1115,9 @@ quantify scope t tvs ty = do
11101115 check m n xs (VFV c (VarFree vs)) = do
11111116 (xs,vs) <- mapAccumM (check m n) xs vs
11121117 return (xs,VFV c (VarFree vs))
1113- check m n xs (VFV c (VarOpts name os)) = do
1114- (xs,os) <- mapAccumM (\ acc (l,v) -> second (l,) <$> check m n acc v) xs os
1115- return (xs,VFV c (VarOpts name os))
1118+ check m n xs (VFV c (VarOpts nty name os)) = do
1119+ (xs,os) <- mapAccumM (\ acc (lty, l,v) -> second (lty, l,) <$> check m n acc v) xs os
1120+ return (xs,VFV c (VarOpts nty name os))
11161121 check m n xs (VAlts v vs) = do
11171122 (xs,v) <- check m n xs v
11181123 (xs,vs) <- mapAccumM (\ xs (v1,v2) -> do (xs,v1) <- check m n xs v1
0 commit comments